Loogle!

Result

Found 65 declarations mentioning CategoryTheory.EnrichedFunctor.

• CategoryTheory.EnrichedFunctor 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] (D : Type u₂) [CategoryTheory.EnrichedCategory V D] : Type (max (max u₁ u₂) w)
• CategoryTheory.EnrichedFunctor.id 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.EnrichedFunctor V C C
• CategoryTheory.EnrichedFunctor.instInhabited 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] : Inhabited (CategoryTheory.EnrichedFunctor V C C)
• CategoryTheory.EnrichedFunctor.category 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] : CategoryTheory.Category.{max u₁ w, max (max u₂ u₁) w} (CategoryTheory.EnrichedFunctor V C D)
• CategoryTheory.EnrichedFunctor.obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) : C → D
• CategoryTheory.EnrichedNatTrans 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (F G : CategoryTheory.EnrichedFunctor V C D) : Type (max u₁ w)
• CategoryTheory.GradedNatTrans 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (A : CategoryTheory.Center V) (F G : CategoryTheory.EnrichedFunctor V C D) : Type (max u₁ w)
• CategoryTheory.enrichedNatTransYoneda 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) : CategoryTheory.Functor Vᵒᵖ (Type (max u₁ w))
• CategoryTheory.enrichedFunctorTypeEquivFunctor 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] : CategoryTheory.EnrichedFunctor (Type v) C D ≃ CategoryTheory.Functor C D
• CategoryTheory.EnrichedFunctor.comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) : CategoryTheory.EnrichedFunctor V C E
• CategoryTheory.EnrichedFunctor.forget 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] (F : CategoryTheory.EnrichedFunctor W C D) : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment W C) (CategoryTheory.ForgetEnrichment W D)
• CategoryTheory.EnrichedFunctor.map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y : C) : (X ⟶[V] Y) ⟶ self.obj X ⟶[V] self.obj Y
• CategoryTheory.EnrichedFunctor.comp_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (X : C) : (CategoryTheory.EnrichedFunctor.comp V F G).obj X = G.obj (F.obj X)
• CategoryTheory.enrichedNatTransYoneda_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) (A : Vᵒᵖ) : (CategoryTheory.enrichedNatTransYoneda F G).obj A = CategoryTheory.GradedNatTrans ((CategoryTheory.Center.ofBraided V).obj (Opposite.unop A)) F G
• CategoryTheory.GradedNatTrans.app 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X : C) : A.fst ⟶ F.obj X ⟶[V] G.obj X
• CategoryTheory.EnrichedFunctor.forget_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] (F : CategoryTheory.EnrichedFunctor W C D) (X : CategoryTheory.ForgetEnrichment W C) : F.forget.obj X = CategoryTheory.ForgetEnrichment.of W (F.obj (CategoryTheory.ForgetEnrichment.to W X))
• CategoryTheory.EnrichedFunctor.isoMk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : F ≅ G
• CategoryTheory.GradedNatTrans.ext 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} {inst✝² : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst✝³ : CategoryTheory.EnrichedCategory V D} {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} {x y : CategoryTheory.GradedNatTrans A F G} (app : x.app = y.app) : x = y
• CategoryTheory.GradedNatTrans.ext_iff 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} {inst✝² : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst✝³ : CategoryTheory.EnrichedCategory V D} {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} {x y : CategoryTheory.GradedNatTrans A F G} : x = y ↔ x.app = y.app
• CategoryTheory.EnrichedFunctor.map_id 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (self.map X X) = CategoryTheory.eId V (self.obj X)
• CategoryTheory.EnrichedNatTrans.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (out : F.forget ⟶ G.forget) : CategoryTheory.EnrichedNatTrans F G
• CategoryTheory.EnrichedNatTrans.out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.EnrichedNatTrans F G) : F.forget ⟶ G.forget
• CategoryTheory.EnrichedFunctor.forgetComp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] {E : Type u₃} [CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D) (G : CategoryTheory.EnrichedFunctor W D E) : (CategoryTheory.EnrichedFunctor.comp W F G).forget ≅ F.forget.comp G.forget
• CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) (X : C) : (CategoryTheory.enrichedFunctorTypeEquivFunctor F).obj X = F.obj X
• CategoryTheory.EnrichedFunctor.map_id_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X : C) {Z : V} (h : (self.obj X ⟶[V] self.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (CategoryTheory.CategoryStruct.comp (self.map X X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V (self.obj X)) h
• CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).obj X = F.obj X
• CategoryTheory.EnrichedFunctor.comp_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (x✝ x✝¹ : C) : (CategoryTheory.EnrichedFunctor.comp V F G).map x✝ x✝¹ = CategoryTheory.CategoryStruct.comp (F.map x✝ x✝¹) (G.map (F.obj x✝) (F.obj x✝¹))
• CategoryTheory.EnrichedFunctor.ext 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.map X Y) (CategoryTheory.eqToHom ⋯) = G.map X Y) : F = G
• CategoryTheory.EnrichedFunctor.category_id_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) : (CategoryTheory.CategoryStruct.id F).out = CategoryTheory.CategoryStruct.id F.forget
• CategoryTheory.EnrichedFunctor.forget_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] (F : CategoryTheory.EnrichedFunctor W C D) {X✝ Y✝ : CategoryTheory.ForgetEnrichment W C} (f : X✝ ⟶ Y✝) : F.forget.map f = CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homTo W f) (F.map (CategoryTheory.ForgetEnrichment.to W X✝) (CategoryTheory.ForgetEnrichment.to W Y✝)))
• CategoryTheory.EnrichedFunctor.isoMk_hom_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : (CategoryTheory.EnrichedFunctor.isoMk h).hom.out = h.hom
• CategoryTheory.EnrichedFunctor.isoMk_inv_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : (CategoryTheory.EnrichedFunctor.isoMk h).inv.out = h.inv
• CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (x✝ x✝¹ : C) : (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).map x✝ x✝¹ = TypeCat.ofHom fun f => F.map f
• CategoryTheory.EnrichedFunctor.category_comp_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {X✝ Y✝ Z✝ : CategoryTheory.EnrichedFunctor V C D} (F : CategoryTheory.EnrichedNatTrans X✝ Y✝) (G : CategoryTheory.EnrichedNatTrans Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp F G).out = CategoryTheory.CategoryStruct.comp F.out G.out
• CategoryTheory.EnrichedFunctor.hom_ext 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} {α β : F ⟶ G} (h : ∀ (X : C), α.out.app X = β.out.app X) : α = β
• CategoryTheory.EnrichedFunctor.hom_ext_iff 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} {α β : F ⟶ G} : α = β ↔ ∀ (X : C), α.out.app X = β.out.app X
• CategoryTheory.EnrichedFunctor.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (obj : C → D) (map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y) (map_id : ∀ (X : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) = CategoryTheory.eId V (obj X) := by cat_disch) (map_comp : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z)) (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)) := by cat_disch) : CategoryTheory.EnrichedFunctor V C D
• CategoryTheory.enrichedNatTransYoneda_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) {X✝ Y✝ : Vᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.enrichedNatTransYoneda F G).map f = TypeCat.ofHom fun σ => { app := fun X => CategoryTheory.CategoryStruct.comp f.unop (σ.app X), naturality := ⋯ }
• CategoryTheory.EnrichedFunctor.map_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (self.map X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z))
• CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type v} [CategoryTheory.EnrichedCategory (Type v) C] {D : Type v} [CategoryTheory.EnrichedCategory (Type v) D] (F G : CategoryTheory.EnrichedFunctor (Type v) C D) : CategoryTheory.enrichedNatTransYoneda F G ≅ CategoryTheory.yoneda.obj (CategoryTheory.enrichedFunctorTypeEquivFunctor F ⟶ CategoryTheory.enrichedFunctorTypeEquivFunctor G)
• CategoryTheory.EnrichedFunctor.forgetComp_hom_app 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] {E : Type u₃} [CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D) (G : CategoryTheory.EnrichedFunctor W D E) (X : CategoryTheory.ForgetEnrichment W C) : (F.forgetComp G).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of W (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to W X))))
• CategoryTheory.EnrichedFunctor.forgetComp_inv_app 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] {E : Type u₃} [CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D) (G : CategoryTheory.EnrichedFunctor W D E) (X : CategoryTheory.ForgetEnrichment W C) : (F.forgetComp G).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of W (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to W X))))
• CategoryTheory.EnrichedFunctor.map_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C) {Z✝ : V} (h : (self.obj X ⟶[V] self.obj Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (CategoryTheory.CategoryStruct.comp (self.map X Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z)) h)
• CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.enrichedFunctorTypeEquivFunctor F).map f = (CategoryTheory.ConcreteCategory.hom (F.map X✝ Y✝)) f
• CategoryTheory.GradedNatTrans.naturality 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X Y : C) : CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))
• CategoryTheory.GradedNatTrans.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X) (naturality : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y)) (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y)) (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))) : CategoryTheory.GradedNatTrans A F G
• CategoryTheory.GradedNatTrans.naturality_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X Y : C) {Z : V} (h : (F.obj X ⟶[V] G.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y)) h)
• CategoryTheory.SimplicialThickening.functor 📋 Mathlib.AlgebraicTopology.SimplicialNerve
  {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) : CategoryTheory.EnrichedFunctor SSet (CategoryTheory.SimplicialThickening J) (CategoryTheory.SimplicialThickening K)
• CategoryTheory.SimplicialThickening.functor_id 📋 Mathlib.AlgebraicTopology.SimplicialNerve
  (J : Type u) [LinearOrder J] : CategoryTheory.SimplicialThickening.functor OrderHom.id = CategoryTheory.EnrichedFunctor.id SSet (CategoryTheory.SimplicialThickening J)
• CategoryTheory.SimplicialThickening.functor_comp 📋 Mathlib.AlgebraicTopology.SimplicialNerve
  {J K L : Type u} [LinearOrder J] [LinearOrder K] [LinearOrder L] (f : J →o K) (g : K →o L) : CategoryTheory.SimplicialThickening.functor (g.comp f) = CategoryTheory.EnrichedFunctor.comp SSet (CategoryTheory.SimplicialThickening.functor f) (CategoryTheory.SimplicialThickening.functor g)
• CategoryTheory.EnrichedCat.leftUnitor 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) : CategoryTheory.EnrichedFunctor.comp V (CategoryTheory.EnrichedFunctor.id V C) F ≅ F
• CategoryTheory.EnrichedCat.rightUnitor 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) : CategoryTheory.EnrichedFunctor.comp V F (CategoryTheory.EnrichedFunctor.id V D) ≅ F
• CategoryTheory.EnrichedCat.associator 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {E' : Type u₃} [CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E') : CategoryTheory.EnrichedFunctor.comp V (CategoryTheory.EnrichedFunctor.comp V F G) H ≅ CategoryTheory.EnrichedFunctor.comp V F (CategoryTheory.EnrichedFunctor.comp V G H)
• CategoryTheory.EnrichedCat.whiskerLeft 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) {G H : CategoryTheory.EnrichedFunctor V D E} (α : G ⟶ H) : CategoryTheory.EnrichedFunctor.comp V F G ⟶ CategoryTheory.EnrichedFunctor.comp V F H
• CategoryTheory.EnrichedCat.whiskerRight 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D} (α : F ⟶ G) (H : CategoryTheory.EnrichedFunctor V D E) : CategoryTheory.EnrichedFunctor.comp V F H ⟶ CategoryTheory.EnrichedFunctor.comp V G H
• CategoryTheory.EnrichedCat.leftUnitor_hom_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.leftUnitor F).hom.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.leftUnitor_inv_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.leftUnitor F).inv.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.rightUnitor_hom_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.rightUnitor F).hom.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.rightUnitor_inv_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.rightUnitor F).inv.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.whisker_exchange 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D} {H I : CategoryTheory.EnrichedFunctor V D E} (α : F ⟶ G) (β : H ⟶ I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerLeft F β) (CategoryTheory.EnrichedCat.whiskerRight α I) = CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerRight α H) (CategoryTheory.EnrichedCat.whiskerLeft G β)
• CategoryTheory.EnrichedCat.whiskerLeft_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) {G H : CategoryTheory.EnrichedFunctor V D E} (α : G ⟶ H) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.whiskerLeft F α).out.app X = α.out.app (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.comp_whiskerRight 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G H : CategoryTheory.EnrichedFunctor V C D} (α : F ⟶ G) (β : G ⟶ H) (I : CategoryTheory.EnrichedFunctor V D E) : CategoryTheory.EnrichedCat.whiskerRight { out := CategoryTheory.CategoryStruct.comp α.out β.out } I = CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerRight α I) (CategoryTheory.EnrichedCat.whiskerRight β I)
• CategoryTheory.EnrichedCat.associator_hom_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {E' : Type u₃} [CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E') (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.associator F G H).hom.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (H.obj (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to V X)))))
• CategoryTheory.EnrichedCat.associator_inv_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {E' : Type u₃} [CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E') (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.associator F G H).inv.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (H.obj (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to V X)))))
• CategoryTheory.EnrichedCat.whiskerRight_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D} (α : F ⟶ G) (H : CategoryTheory.EnrichedFunctor V D E) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.whiskerRight α H).out.app X = CategoryTheory.ForgetEnrichment.homOf V (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homTo V (α.out.app X)) (H.map (F.obj (CategoryTheory.ForgetEnrichment.to V X)) (G.obj (CategoryTheory.ForgetEnrichment.to V X))))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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 ?a

   If 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 ?b

4. By 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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c