no goals
C : Type u
inst✝⁸ : Category C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : Functor.PreservesZeroMorphisms G
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
rw [← G.map_comp, hpq, G.map_comp]
no goals
C : Type u
inst✝⁸ : Category C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : Functor.PreservesZeroMorphisms G
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f) ≫ G.map f = 0
rw [← G.map_comp, kernel.condition, G.map_zero]
no goals
C : Type u
inst✝⁸ : Category C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : Functor.PreservesZeroMorphisms G
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι g) ≫ G.map g = 0
rw [← G.map_comp, kernel.condition, G.map_zero]
C : Type u
inst✝⁸ : Category C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : Functor.PreservesZeroMorphisms G
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f ≫ p) = G.map (kernel.map f g p q hpq ≫ kernel.ι g)
C : Type u
inst✝⁸ : Category C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : Functor.PreservesZeroMorphisms G
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f) ≫ G.map p = G.map (kernel.map f g p q hpq) ≫ G.map (kernel.ι g)
simp only [← G.map_comp]
no goals
C : Type u
inst✝⁸ : Category C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : Functor.PreservesZeroMorphisms G
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f ≫ p) = G.map (kernel.map f g p q hpq ≫ kernel.ι g)
exact G.congr_map (kernel.lift_ι _ _ _).symm