Loogle!

Result

Found 15 declarations mentioning CategoryTheory.EnrichedFunctor.map.

• CategoryTheory.EnrichedFunctor.id_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] (x✝ x✝¹ : C) : (CategoryTheory.EnrichedFunctor.id V C).map x✝ x✝¹ = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom x✝ x✝¹)
• 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) : CategoryTheory.EnrichedCategory.Hom X Y ⟶ CategoryTheory.EnrichedCategory.Hom (self.obj X) (self.obj Y)
• 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.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 = F.map X✝ Y✝ f
• 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 : CategoryTheory.EnrichedCategory.Hom (self.obj X) (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_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) (f : CategoryTheory.EnrichedCategory.Hom x✝ x✝¹) : (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).map x✝ x✝¹ f = F.map f
• 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.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.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 : CategoryTheory.EnrichedCategory.Hom (self.obj X) (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.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.β (CategoryTheory.EnrichedCategory.Hom X 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 ⟶ CategoryTheory.EnrichedCategory.Hom (F.obj X) (G.obj X)) (naturality : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (A.snd.β (CategoryTheory.EnrichedCategory.Hom X 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.mk.sizeOf_spec 📋 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} [SizeOf V] [SizeOf C] [SizeOf D] (app : (X : C) → A.fst ⟶ CategoryTheory.EnrichedCategory.Hom (F.obj X) (G.obj X)) (naturality : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (A.snd.β (CategoryTheory.EnrichedCategory.Hom X 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))) : sizeOf { app := app, naturality := naturality } = 1
• 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.GradedNatTrans.mk.injEq 📋 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 ⟶ CategoryTheory.EnrichedCategory.Hom (F.obj X) (G.obj X)) (naturality : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (A.snd.β (CategoryTheory.EnrichedCategory.Hom X 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))) (app✝ : (X : C) → A.fst ⟶ CategoryTheory.EnrichedCategory.Hom (F.obj X) (G.obj X)) (naturality✝ : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (A.snd.β (CategoryTheory.EnrichedCategory.Hom X 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))) : ({ app := app, naturality := naturality } = { app := app✝, naturality := naturality✝ }) = (app = app✝)
• CategoryTheory.SimplicialThickening.functor_map 📋 Mathlib.AlgebraicTopology.SimplicialNerve
  {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) (i j : CategoryTheory.SimplicialThickening J) : (CategoryTheory.SimplicialThickening.functor f).map i j = CategoryTheory.nerveMap (CategoryTheory.SimplicialThickening.functorMap f i j)

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:

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.

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 19971e9 serving mathlib revision 40fea08