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✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (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✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map (coequalizer.π f 0) = 0
rw [← G.map_comp, cokernel.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✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map g ≫ G.map (coequalizer.π g 0) = 0
rw [← G.map_comp, cokernel.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✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (coequalizer.π f 0 ≫ cokernel.map f g p q hpq) = G.map (q ≫ coequalizer.π g 0)
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✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (coequalizer.π f 0) ≫ G.map (cokernel.map f g p q hpq) = G.map q ≫ G.map (coequalizer.π g 0)
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✝³ : HasCokernel f
inst✝² : HasCokernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasCokernel g
inst✝ : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (coequalizer.π f 0 ≫ cokernel.map f g p q hpq) = G.map (q ≫ coequalizer.π g 0)
exact G.congr_map (cokernel.π_desc _ _ _)