C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Epi (L.map f)
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (L.map f)
letI := preservesZeroMorphisms_of_map_exact L h
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact (L.map f) 0
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Epi (L.map f)
apply ((tfae_epi (L.obj 0) (L.map f)).out 2 0).mp
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact (L.map f) (L.map 0)
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact (L.map f) 0
rw [← L.map_zero]
no goals
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Abelian C
A : Type u₁
B : Type u₂
inst✝³ : Category A
inst✝² : Category B
inst✝¹ : Abelian A
inst✝ : Abelian B
L : A ⥤ B
h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, Exact f g → Exact (L.map f) (L.map g)
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
this : PreservesZeroMorphisms L := preservesZeroMorphisms_of_map_exact L h
⊢ Exact (L.map f) (L.map 0)
exact h (((tfae_epi 0 f).out 0 2).mp hf)