Equivalence between subobjects and quotients in an abelian category

noncomputable def CategoryTheory.Abelian.subobjectIsoSubobjectOp {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : Subobject X ≃o (Subobject (Opposite.op X))ᵒᵈ

In an abelian category, the subobjects and quotient objects of an object X are order-isomorphic via taking kernels and cokernels. Implemented here using subobjects in the opposite category, since mathlib does not have a notion of quotient objects at the time of writing.

Equations

• CategoryTheory.Abelian.subobjectIsoSubobjectOp X = OrderIso.ofHomInv (CategoryTheory.Limits.cokernelOrderHom X) (CategoryTheory.Limits.kernelOrderHom X) ⋯ ⋯

@[simp]

theorem CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (a : (Subobject (Opposite.op X))ᵒᵈ) : (RelIso.symm (subobjectIsoSubobjectOp X)) a = Subobject.lift (fun (x : Cᵒᵖ) (f : x ⟶ Opposite.op X) (x_1 : Mono f) => Subobject.mk (Limits.kernel.ι f.unop)) ⋯ a

@[simp]

theorem CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (a : Subobject X) : (subobjectIsoSubobjectOp X) a = Subobject.lift (fun (x : C) (f : x ⟶ X) (x_1 : Mono f) => Subobject.mk (Limits.cokernel.π f).op) ⋯ a

instance CategoryTheory.Abelian.wellPowered_opposite {C : Type u} [Category.{v, u} C] [Abelian C] [LocallySmall.{w, v, u} C] [WellPowered.{w, v, u} C] : WellPowered.{w, v, u} Cᵒᵖ

A well-powered abelian category is also well-copowered.

instance CategoryTheory.Abelian.instEpiPullbackπ {C : Type u} [Category.{v, u} C] [Abelian C] {X Y : C} (f : X ⟶ Y) [Epi f] (B : Subobject Y) : Epi (Subobject.pullbackπ f B)

In an abelian category, the projection Subobject.pullbackπ f B from the pullback of a subobject B along an epimorphism f is an epimorphism.