mathlib documentation

category_theory.balanced

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.

@[class]
structure category_theory.balanced (C : Type u) [category_theory.category C] :
Prop

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

Instances of this typeclass