Equivalence between subobjects and quotients in an abelian category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
noncomputable
def
category_theory.abelian.subobject_iso_subobject_op
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(X : C) :
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.
@[simp]
theorem
category_theory.abelian.subobject_iso_subobject_op_apply
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(X : C)
(a : category_theory.subobject X) :
⇑(category_theory.abelian.subobject_iso_subobject_op X) a = category_theory.subobject.lift (λ (A : C) (f : A ⟶ X) (hf : category_theory.mono f), category_theory.subobject.mk (category_theory.limits.cokernel.π f).op) _ a
@[simp]
theorem
category_theory.abelian.subobject_iso_subobject_op_symm_apply
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(X : C)
(a : (category_theory.subobject (opposite.op X))ᵒᵈ) :
⇑(rel_iso.symm (category_theory.abelian.subobject_iso_subobject_op X)) a = category_theory.subobject.lift (λ (A : Cᵒᵖ) (f : A ⟶ opposite.op X) (hf : category_theory.mono f), category_theory.subobject.mk (category_theory.limits.kernel.ι f.unop)) _ a
@[protected, instance]
def
category_theory.abelian.well_powered_opposite
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
[category_theory.well_powered C] :
A well-powered abelian category is also well-copowered.