Skip to content

Commit fef0cd0

Browse files
committed
chore(Algebra/Homology): remove unnecessary ReflectsEpimorphisms instance (#14200)
1 parent 3d4d0ed commit fef0cd0

File tree

1 file changed

+0
-12
lines changed

1 file changed

+0
-12
lines changed

Mathlib/Algebra/Homology/ShortComplex/Exact.lean

-12
Original file line numberDiff line numberDiff line change
@@ -934,25 +934,13 @@ instance : F.PreservesMonomorphisms where
934934
exact ((S.map F).exact_iff_mono (by simp)).1
935935
(((S.exact_iff_mono rfl).2 hf).map F)
936936

937-
instance [Faithful F] [CategoryWithHomology C] : F.ReflectsMonomorphisms where
938-
reflects {X Y} f hf := by
939-
let S := ShortComplex.mk (0 : X ⟶ X) f zero_comp
940-
exact (S.exact_iff_mono rfl).1
941-
((ShortComplex.exact_map_iff_of_faithful S F).1
942-
(((S.map F).exact_iff_mono (by simp)).2 hf))
943937

944938
instance : F.PreservesEpimorphisms where
945939
preserves {X Y} f hf := by
946940
let S := ShortComplex.mk f (0 : Y ⟶ Y) comp_zero
947941
exact ((S.map F).exact_iff_epi (by simp)).1
948942
(((S.exact_iff_epi rfl).2 hf).map F)
949943

950-
instance [Faithful F] [CategoryWithHomology C] : F.ReflectsEpimorphisms where
951-
reflects {X Y} f hf := by
952-
let S := ShortComplex.mk f (0 : Y ⟶ Y) comp_zero
953-
exact (S.exact_iff_epi rfl).1
954-
((ShortComplex.exact_map_iff_of_faithful S F).1
955-
(((S.map F).exact_iff_epi (by simp)).2 hf))
956944

957945
end Functor
958946

0 commit comments

Comments
 (0)