Loogle!

Result

Found 16 declarations mentioning CategoryTheory.Limits.cokernel.map.

• CategoryTheory.Limits.cokernel.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel f'] (p : X ⟶ X') (q : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f') : CategoryTheory.Limits.cokernel f ⟶ CategoryTheory.Limits.cokernel f'
• CategoryTheory.Limits.cokernel.mapIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f') : (CategoryTheory.Limits.cokernel.mapIso f f' p q w).hom = CategoryTheory.Limits.cokernel.map f f' p.hom q.hom w
• CategoryTheory.Limits.cokernel.mapIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f') : (CategoryTheory.Limits.cokernel.mapIso f f' p q w).inv = CategoryTheory.Limits.cokernel.map f' f p.inv q.inv ⋯
• CategoryTheory.Limits.cokernel.map_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel f'] (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f') (h₂ : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map f f' p q h₁) (CategoryTheory.Limits.cokernel.desc f' g' w') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f g w) r
• CategoryTheory.Limits.cokernel_map_comp_cokernelComparison 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X' Y' : C} [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasCokernel (G.map f)] (g : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel g] [CategoryTheory.Limits.HasCokernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) (CategoryTheory.Limits.cokernelComparison g G) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G) (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq))
• CategoryTheory.Limits.cokernel_map_comp_cokernelComparison_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X' Y' : C} [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasCokernel (G.map f)] (g : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel g] [CategoryTheory.Limits.HasCokernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) {Z : D} (h : G.obj (CategoryTheory.Limits.cokernel g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison g G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G) (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq)) h)
• CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasCokernel (G.map f)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] {X' Y' : C} (g : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel g] [CategoryTheory.Limits.HasCokernel (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G f).hom (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq)) (CategoryTheory.Limits.PreservesCokernel.iso G g).hom
• CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasCokernel (G.map f)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] {X' Y' : C} (g : X' ⟶ Y') [CategoryTheory.Limits.HasCokernel g] [CategoryTheory.Limits.HasCokernel (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) {Z : D} (h : CategoryTheory.Limits.cokernel (G.map g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G g).hom h)
• CategoryTheory.Abelian.coimageImageComparisonFunctor_map 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {f g : CategoryTheory.Arrow C} (η : f ⟶ g) : CategoryTheory.Abelian.coimageImageComparisonFunctor.map η = CategoryTheory.Arrow.homMk (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.Limits.kernel.ι g.hom) (CategoryTheory.Limits.kernel.map f.hom g.hom η.left η.right ⋯) η.left ⋯) (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π f.hom) (CategoryTheory.Limits.cokernel.π g.hom) η.right (CategoryTheory.Limits.cokernel.map f.hom g.hom η.left η.right ⋯) ⋯) ⋯
• CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι (α.app X)) ((CategoryTheory.Limits.kernel.ι α).app X) (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) α).inv (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯) (CategoryTheory.Limits.cokernelComparison (CategoryTheory.Limits.kernel.ι α) ((CategoryTheory.evaluation C D).obj X))
• CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso ((CategoryTheory.evaluation C D).obj X) (CategoryTheory.Limits.kernel.ι α)).hom (CategoryTheory.Limits.cokernel.map ((CategoryTheory.Limits.kernel.ι α).app X) (CategoryTheory.Limits.kernel.ι (α.app X)) (CategoryTheory.Limits.kernelComparison α ((CategoryTheory.evaluation C D).obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯)
• CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₃.f = CategoryTheory.Limits.cokernel.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) g ⋯
• CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₃.g = CategoryTheory.Limits.cokernel.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id Z) ⋯
• CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₁ = CategoryTheory.Limits.cokernel.π f
• CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₃ = CategoryTheory.Limits.cokernel.π g
• CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂ 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₂ = CategoryTheory.kernelCokernelCompSequence.π f g

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 bce1d65