Kernel monotonicity for setoids #
Mirror of Mathlib/Data/Setoid/Basic.lean: the composition-monotonicity
of Setoid.ker. Mathlib has this fact for every algebraic kernel —
LinearMap.ker_le_ker_comp (whose name this mirrors), MonoidHom.comap_ker,
RingHom.comap_ker, CategoryTheory.Limits.kernelSubobject_comp_le — but
not for the plain Setoid.ker they all specialize. [UPSTREAM]
theorem
Setoid.ker_le_ker_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(h : β → γ)
:
If g factors through f, then the kernel of f refines the kernel
of g — the Setoid primitive of LinearMap.ker_le_ker_comp. [UPSTREAM]