English
A kernel-preserving functor preserves equalizers: for any morphisms f,g: X → Y, the equalizer of f and g is preserved by F.
Русский
Функтор, сохраняющий ядра, сохраняет равноселители: для любых f,g: X → Y равноселитель сохраняется Ф.
LaTeX
$$$PreservesLimit( parallelPair(f,g), F)$ for all $f,g$$$
Lean4
/-- A functor between preadditive categories preserves the equalizer of two
morphisms if it preserves all kernels. -/
theorem preservesEqualizer_of_preservesKernels [∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F] {X Y : C}
(f g : X ⟶ Y) : PreservesLimit (parallelPair f g) F :=
by
letI := preservesBinaryBiproducts_of_preservesBinaryProducts F
haveI := additive_of_preservesBinaryBiproducts F
constructor; intro c i
let c' := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
dsimp only [kernelForkOfFork_ofι] at c'
let iFc := isLimitForkMapOfIsLimit' F _ c'
constructor
apply IsLimit.ofIsoLimit _ ((Cones.functoriality _ F).mapIso (Fork.isoForkOfι c).symm)
apply (isLimitMapConeForkEquiv F (Fork.condition c)).invFun
let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq F.map_sub rfl
exact
IsLimit.ofIsoLimit (isLimitForkOfKernelFork ((IsLimit.postcomposeHomEquiv p _).symm iFc))
(Fork.ext (Iso.refl _) (by simp [p]))
