feat(category_theory): separators and detectors (#11880)

src/category_theory/balanced.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import category_theory.isomorphism
+import category_theory.epi_mono
 
 /-!
 # Balanced categories
@@ -14,10 +14,6 @@ Balanced categories arise frequently. For example, categories in which every mon
 (or epimorphism) is strong are balanced. Examples of this are abelian categories and toposes, such
 as the category of types.
 
-## TODO
-
-The opposite of a balanced category is again balanced.
-
 -/
 
 universes v u
@@ -40,4 +36,13 @@ balanced.is_iso_of_mono_of_epi _
 lemma is_iso_iff_mono_and_epi [balanced C] {X Y : C} (f : X ⟶ Y) : is_iso f ↔ mono f ∧ epi f :=
 ⟨λ _, by exactI ⟨infer_instance, infer_instance⟩, λ ⟨_, _⟩, by exactI is_iso_of_mono_of_epi _⟩
 
+section
+local attribute [instance] is_iso_of_mono_of_epi
+
+lemma balanced_opposite [balanced C] : balanced Cᵒᵖ :=
+{ is_iso_of_mono_of_epi := λ X Y f fmono fepi,
+    by { rw ← quiver.hom.op_unop f, exactI is_iso_of_op _ } }
+
+end
+
 end category_theory