# Balanced categories #

A category is called balanced if any morphism that is both monic and epic is an isomorphism.

Balanced categories arise frequently. For example, categories in which every monomorphism (or epimorphism) is strong are balanced. Examples of this are abelian categories and toposes, such as the category of types.

source
class CategoryTheory.Balanced (C : Type u) [Category.{v, u} C] :
Prop

A category is called balanced if any morphism that is both monic and epic is an isomorphism.

- isIso_of_mono_of_epi {X Y : C} (f : X ⟶ Y) [Mono f] [Epi f] : IsIso f

Instances

source
theorem CategoryTheory.isIso_of_mono_of_epi {C : Type u} [Category.{v, u} C] [Balanced C] {X Y : C} (f : X ⟶ Y) [Mono f] [Epi f] :
IsIso f
source
theorem CategoryTheory.isIso_iff_mono_and_epi {C : Type u} [Category.{v, u} C] [Balanced C] {X Y : C} (f : X ⟶ Y) :
IsIso f ↔ Mono f ∧ Epi f
source
instance CategoryTheory.balanced_opposite {C : Type u} [Category.{v, u} C] [Balanced C] :
Balanced C ᵒᵖ