English
Given f with kernels and G with kernels, and g, p, q with hpq, an equality of composed maps holds: kernelComparison f G ≫ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by ...) = G.map (kernel.map f g p q hpq) ≫ kernelComparison g G.
Русский
При наличии ядер f и G, а также гомоморфизмов g, p, q и hpq выполняется равенство композиции: kernelComparison f G ≫ kernel.map ... = G.map (kernel.map f g p q hpq) ≫ kernelComparison g G.
LaTeX
$$$kernelComparison f G \;\circ\; kernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [\u2190 G.map_comp, hpq, G.map_comp]) = G.map (kernel.map f g p q hpq) \circ\; kernelComparison g G$$$
Lean4
@[reassoc]
theorem kernelComparison_comp_kernel_map {X' Y' : C} [HasKernel f] [HasKernel (G.map f)] (g : X' ⟶ Y') [HasKernel g]
[HasKernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : f ≫ q = p ≫ g) :
kernelComparison f G ≫ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [← G.map_comp, hpq, G.map_comp]) =
G.map (kernel.map f g p q hpq) ≫ kernelComparison g G :=
kernel.lift_map _ _ (by rw [← G.map_comp, kernel.condition, G.map_zero]) _ _
(by rw [← G.map_comp, kernel.condition, G.map_zero]) _ _ _
(by simp only [← G.map_comp]; exact G.congr_map (kernel.lift_ι _ _ _).symm) _
