Theorems · Definition · category theory

CategoryTheory.Limits.IsZero.to_

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → CategoryTheory.Limits.IsZero X → (Y : C) → X ⟶ Y

If h : IsZero X, then h.to_ Y is a choice of unique morphism X → Y. to is a reserved word, it was replaced by to_

Defined in

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Cited by

8 results in Mathlib

Foundations

Depth 3 from the axioms · uses Classical.choice

Assumes

CategoryTheory.Category