case w.h
C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ (plusMap J 0).app x✝ = 0.app x✝
C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
⊢ plusMap J 0 = 0
ext : 2
case w.h
C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
S : (Cover J x✝.unop)ᵒᵖ
⊢ colimit.ι (diagram J P x✝.unop) S ≫ (plusMap J 0).app x✝ = colimit.ι (diagram J P x✝.unop) S ≫ 0.app x✝
case w.h
C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ (plusMap J 0).app x✝ = 0.app x✝
refine' colimit.hom_ext (fun S => _)
no goals
case w.h
C : Type u
inst✝⁴ : Category C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
S : (Cover J x✝.unop)ᵒᵖ
⊢ colimit.ι (diagram J P x✝.unop) S ≫ (plusMap J 0).app x✝ = colimit.ι (diagram J P x✝.unop) S ≫ 0.app x✝
erw [comp_zero, colimit.ι_map, J.diagramNatTrans_zero, zero_comp]