Loogle!

Result

Found 15 declarations mentioning CategoryTheory.WithInitial.map.

• CategoryTheory.WithInitial.map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.WithInitial C) (CategoryTheory.WithInitial D)
• CategoryTheory.WithInitial.mapId 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.WithInitial.map (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.WithInitial C)
• CategoryTheory.WithInitial.mapComp 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) : CategoryTheory.WithInitial.map (F.comp G) ≅ (CategoryTheory.WithInitial.map F).comp (CategoryTheory.WithInitial.map G)
• CategoryTheory.WithInitial.pseudofunctor_mapId 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithInitial.pseudofunctor.mapId C = CategoryTheory.WithInitial.mapId ↑C
• CategoryTheory.WithInitial.map_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.map F).obj X = match X with | CategoryTheory.WithInitial.of x => CategoryTheory.WithInitial.of (F.obj x) | CategoryTheory.WithInitial.star => CategoryTheory.WithInitial.star
• CategoryTheory.WithInitial.map₂ 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) : CategoryTheory.WithInitial.map F ⟶ CategoryTheory.WithInitial.map G
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {X✝ Y✝ : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑X✝ ↑Y✝) : CategoryTheory.WithInitial.prelaxfunctor.map F = CategoryTheory.WithInitial.map F
• CategoryTheory.WithInitial.pseudofunctor_mapComp 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ c✝ : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑a✝ ↑b✝) (G : CategoryTheory.Functor ↑b✝ ↑c✝) : CategoryTheory.WithInitial.pseudofunctor.mapComp F G = CategoryTheory.WithInitial.mapComp F G
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂ 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) : CategoryTheory.WithInitial.prelaxfunctor.map₂ η = CategoryTheory.WithInitial.map₂ η
• CategoryTheory.WithInitial.mapId_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.mapId C).hom.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of a) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
• CategoryTheory.WithInitial.mapId_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.mapId C).inv.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of a) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
• CategoryTheory.WithInitial.map₂_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.map₂ η).app X = match X with | CategoryTheory.WithInitial.of x => η.app x | CategoryTheory.WithInitial.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star
• CategoryTheory.WithInitial.map_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) : (CategoryTheory.WithInitial.map F).map f = match X, Y, f with | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => PUnit.unit | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => PUnit.unit
• CategoryTheory.WithInitial.mapComp_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.mapComp F G).hom.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj a))) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
• CategoryTheory.WithInitial.mapComp_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.mapComp F G).inv.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj a))) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv

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