Loogle!

Result

Found 12 declarations mentioning CategoryTheory.ComposableArrows.Precomp.map.

• CategoryTheory.ComposableArrows.Precomp.map_id 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (i : Fin (n + 1 + 1)) : CategoryTheory.ComposableArrows.Precomp.map F f i i ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Precomp.obj F X i)
• CategoryTheory.ComposableArrows.Precomp.map 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (i j : Fin (n + 1 + 1)) : i ≤ j → (CategoryTheory.ComposableArrows.Precomp.obj F X i ⟶ CategoryTheory.ComposableArrows.Precomp.obj F X j)
• CategoryTheory.ComposableArrows.Precomp.map_zero_one' 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) : CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨0 + 1, ⋯⟩ ⋯ = f
• CategoryTheory.ComposableArrows.Precomp.map_succ_succ 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (i j : ℕ) (hi : i + 1 < n + 1 + 1) (hj : j + 1 < n + 1 + 1) (hij : i + 1 ≤ j + 1) : CategoryTheory.ComposableArrows.Precomp.map F f ⟨i + 1, hi⟩ ⟨j + 1, hj⟩ hij = F.map' i j ⋯ ⋯
• CategoryTheory.ComposableArrows.Precomp.map_one_succ 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (j : ℕ) (hj : j + 1 < n + 1 + 1) : CategoryTheory.ComposableArrows.Precomp.map F f 1 ⟨j + 1, hj⟩ ⋯ = F.map' 0 j ⋯ ⋯
• CategoryTheory.ComposableArrows.Precomp.map_comp 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) {i j k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k) : CategoryTheory.ComposableArrows.Precomp.map F f i k ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Precomp.map F f i j hij) (CategoryTheory.ComposableArrows.Precomp.map F f j k hjk)
• CategoryTheory.ComposableArrows.Precomp.map_zero_one 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) : CategoryTheory.ComposableArrows.Precomp.map F f 0 1 ⋯ = f
• CategoryTheory.ComposableArrows.Precomp.map_zero_zero 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) : CategoryTheory.ComposableArrows.Precomp.map F f 0 0 ⋯ = CategoryTheory.CategoryStruct.id X
• CategoryTheory.ComposableArrows.precomp_map 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) {X✝ Y✝ : Fin (n + 1 + 1)} (g : X✝ ⟶ Y✝) : (F.precomp f).map g = CategoryTheory.ComposableArrows.Precomp.map F f X✝ Y✝ ⋯
• CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (j : ℕ) (hj : j + 2 < n + 1 + 1) : CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨j + 2, hj⟩ ⋯ = CategoryTheory.CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯)
• CategoryTheory.ComposableArrows.Precomp.map_one_one 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) : CategoryTheory.ComposableArrows.Precomp.map F f 1 1 ⋯ = F.map (CategoryTheory.CategoryStruct.id ⟨0, ⋯⟩)
• CategoryTheory.ShortComplex.toComposableArrows_map 📋 Mathlib.Algebra.Homology.ExactSequence
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) {X✝ Y✝ : Fin (1 + 1 + 1)} (g : X✝ ⟶ Y✝) : S.toComposableArrows.map g = CategoryTheory.ComposableArrows.Precomp.map (CategoryTheory.ComposableArrows.mk₁ S.g) S.f X✝ Y✝ ⋯

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.

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 88c39f3 serving mathlib revision 9977002