Theorems · Definition · category theory

CategoryTheory.Limits.Cofan.inj

{β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] → {f : β → C} → (p : CategoryTheory.Limits.Cofan f) → (j : β) → f j ⟶ p.pt

Get the jth "injection" in the cofan. (Note that the initial letter of inj matches the greek letter in Cocone.ι.)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

170 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 126 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category