English
If a pair (a, b) is the kernel pair for f1 : X → Y and f2 : Y → Z is mono, then the same pair (a, b) is a kernel pair for the composite f1 ≫ f2.
Русский
Если пара морфизмов (a, b) является парой ядра для f1: X → Y и f2: Y → Z моно, то эта же пара (a, b) образует пару ядра для композиции f1 ≫ f2.
LaTeX
$$$\\forall {C} [\\mathcal{C}], \\forall X,Y,Z,R, f_1:X\\to Y, f_2:Y\\to Z, (\\text{Mono}(f_2)) \\;\\land\\; \\operatorname{IsKernelPair}(f_1,a,b) \\Rightarrow \\operatorname{IsKernelPair}(f_1\\circ f_2, a, b).$$$
Lean4
/-- If `(a,b)` is a kernel pair for `f₁` and `f₂` is mono, then `(a,b)` is a kernel pair for `f₁ ≫ f₂`.
The converse of `cancel_right_of_mono`.
-/
theorem comp_of_mono {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} [Mono f₂] (small_k : IsKernelPair f₁ a b) : IsKernelPair (f₁ ≫ f₂) a b :=
{ w := by rw [small_k.w_assoc]
isLimit' :=
⟨by
refine
PullbackCone.isLimitAux _
(fun s => small_k.lift s.fst s.snd (by rw [← cancel_mono f₂, assoc, s.condition, assoc])) (by simp)
(by simp) ?_
intro s m hm
apply small_k.isLimit.hom_ext
apply PullbackCone.equalizer_ext small_k.cone _ _
· exact (hm WalkingCospan.left).trans (by simp)
· exact (hm WalkingCospan.right).trans (by simp)⟩ }
