How to find universal properties?

Stream: new members

[Jujian Zhang]

I am familiarizing myself with category_theory part of library. I am lost on how to find various universal properties of categorical constructions. For example, the universal property of kernel:

import category_theory.abelian.basic

open category_theory
open category_theory.abelian
open category_theory.limits

open_locale zero_object

variables {𝒞 : Type*} [category 𝒞] [abelian 𝒞]

variables {A B K' : 𝒞} {f : A ⟶ B} {ι' : K' ⟶ A}
variables (eq_zero : ι' ≫ f = 0)

example : ∃!(u : K' ≅ kernel f), (u.hom ≫ kernel.ι f = ι') := sorry

[Johan Commelin]

Your K' isn't going to be isomorphic to the kernel in general. You need more conditions for that.

[Johan Commelin]

But you can get a morphism

[Johan Commelin]

There should be a kernel.lift

[Jujian Zhang]

I thought this is the universal property of kernels. I copied it from Wikipedia.

[David Wärn]

It's usually a good idea to have a look at the file where the construction is defined, in this case file#category_theory/limits/shapes/kernels. The docstring at the top explains the API.

What you posted can be called "the universal property of kernels" (except as Johan pointed out, K' ≅ kernel f should read K' ⟶ kernel f), but note that there are usually a couple different equivalent ways of stating a universal property. Mathlib's kernel API is divided into more components: docs#category_theory.limits.kernel.lift will give you the function u, kernel.lift_ι gives you its defining property, and I believe there should be an instance saying that kernel.ι is mono which gives you uniqueness.