Balanced categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
- is_iso_of_mono_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.mono f] [_inst_3 : category_theory.epi f], category_theory.is_iso f
A category is called balanced if any morphism that is both monic and epic is an isomorphism.
Instances of this typeclass
theorem
category_theory.is_iso_of_mono_of_epi
{C : Type u}
[category_theory.category C]
[category_theory.balanced C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
[category_theory.epi f] :
theorem
category_theory.is_iso_iff_mono_and_epi
{C : Type u}
[category_theory.category C]
[category_theory.balanced C]
{X Y : C}
(f : X ⟶ Y) :
theorem
category_theory.balanced_opposite
{C : Type u}
[category_theory.category C]
[category_theory.balanced C] :