C : Type u₁
inst✝⁷ : Category C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom ≫ kernel.ι (G.map f) = kernelComparison f G ≫ kernel.ι (G.map f)
C : Type u₁
inst✝⁷ : Category C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom = kernelComparison f G
rw [← cancel_mono (kernel.ι _)]
no goals
C : Type u₁
inst✝⁷ : Category C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom ≫ kernel.ι (G.map f) = kernelComparison f G ≫ kernel.ι (G.map f)
simp [PreservesKernel.iso]