kernelSubobject_comp_le — Mathlib

English

For f: X → Y with HasKernel f and h: Y → Z with HasKernel (f ≫ h), the kernel subobject of f is contained in the kernel subobject of f ≫ h: kernelSubobject f ≤ kernelSubobject (f ≫ h).

Русский

Пусть f: X → Y имеет ядро, и h: Y → Z с ядром (f ≫ h). Тогда подстановочный ядро ker f вложено в ker(f ≫ h).

LaTeX

$$$\operatorname{kernelSubobject}(f) \leq \operatorname{kernelSubobject}(f \circ h)$$$

Lean4

/-- The kernel of `f` is always a smaller subobject than the kernel of `f ≫ h`. -/
theorem kernelSubobject_comp_le (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) [HasKernel (f ≫ h)] :
    kernelSubobject f ≤ kernelSubobject (f ≫ h) :=
  le_kernelSubobject _ _ (by simp)

Похожие утверждения