HepLean Documentation

Mathlib.CategoryTheory.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.

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

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

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