English
If (a,b) is a kernel pair for f1 ≫ f2 and a ≫ f1 = b ≫ f1, then (a,b) is a kernel pair for f1.
Русский
Если (a,b) образуют KernelPair для f1 ≫ f2 и a ≫ f1 = b ≫ f1, тогда (a,b) образуют KernelPair для f1.
LaTeX
$${ f1 : X ⟶ Y, f2 : Y ⟶ Z, comm : a ⟶ f1 = b ⟶ f1, big_k : IsKernelPair (f1 ≫ f2) a b } → IsKernelPair f1 a b$$
Lean4
/-- If `(a,b)` is a kernel pair for `f₁ ≫ f₂` and `a ≫ f₁ = b ≫ f₁`, then `(a,b)` is a kernel pair for
just `f₁`.
That is, to show that `(a,b)` is a kernel pair for `f₁` it suffices to only show the square
commutes, rather than to additionally show it's a pullback.
-/
theorem cancel_right {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} (comm : a ≫ f₁ = b ≫ f₁) (big_k : IsKernelPair (f₁ ≫ f₂) a b) :
IsKernelPair f₁ a b :=
{ w := comm
isLimit' :=
⟨PullbackCone.isLimitAux' _ fun s =>
by
let s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd (s.condition_assoc _)
refine
⟨big_k.isLimit.lift s', big_k.isLimit.fac _ WalkingCospan.left, big_k.isLimit.fac _ WalkingCospan.right,
fun m₁ m₂ => ?_⟩
apply big_k.isLimit.hom_ext
refine (PullbackCone.mk a b ?_ : PullbackCone (f₁ ≫ f₂) _).equalizer_ext ?_ ?_
· apply reassoc_of% comm
· apply m₁.trans (big_k.isLimit.fac s' WalkingCospan.left).symm
· apply m₂.trans (big_k.isLimit.fac s' WalkingCospan.right).symm⟩ }
