Mathlib.CategoryTheory.Balanced

Module docstring

{"# 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.

CategoryTheory.Balanced structure

Full source

/-- A category is called balanced if any morphism that is both monic and epic is an isomorphism. -/
class Balanced : Prop where
  isIso_of_mono_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Mono f] [Epi f], IsIso f

Balanced category

Informal description

A category $\mathcal{C}$ is called *balanced* if every morphism that is both a monomorphism and an epimorphism is an isomorphism.

CategoryTheory.isIso_of_mono_of_epi theorem

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

Full source

theorem isIso_of_mono_of_epi [Balanced C] {X Y : C} (f : X ⟶ Y) [Mono f] [Epi f] : IsIso f :=
  Balanced.isIso_of_mono_of_epi _

Monomorphic and Epimorphic Morphisms are Isomorphisms in Balanced Categories

Informal description

Let $\mathcal{C}$ be a balanced category. For any morphism $f : X \to Y$ in $\mathcal{C}$ that is both a monomorphism and an epimorphism, $f$ is an isomorphism.

CategoryTheory.isIso_iff_mono_and_epi theorem

[Balanced C] {X Y : C} (f : X ⟶ Y) : IsIso f ↔ Mono f ∧ Epi f

Full source

theorem isIso_iff_mono_and_epi [Balanced C] {X Y : C} (f : X ⟶ Y) : IsIsoIsIso f ↔ Mono f ∧ Epi f :=
  ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => isIso_of_mono_of_epi _⟩

Isomorphism Characterization in Balanced Categories: $f$ is iso iff mono and epi

Informal description

Let $\mathcal{C}$ be a balanced category. For any morphism $f : X \to Y$ in $\mathcal{C}$, $f$ is an isomorphism if and only if it is both a monomorphism and an epimorphism.

CategoryTheory.balanced_opposite instance

[Balanced C] : Balanced Cᵒᵖ

Full source

instance balanced_opposite [Balanced C] : Balanced Cᵒᵖ :=
  { isIso_of_mono_of_epi := fun f fmono fepi => by
      rw [← Quiver.Hom.op_unop f]
      exact isIso_of_op _ }

Opposite of a Balanced Category is Balanced

Informal description

For any balanced category $\mathcal{C}$, its opposite category $\mathcal{C}^{\mathrm{op}}$ is also balanced.