Equivalence between subobjects and quotients in an abelian category #
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
Instances For
@[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]
:
A well-powered abelian category is also well-copowered.