Equivalence between subobjects and quotients in an abelian category #
@[simp]
theorem
CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(X : C)
(a : CategoryTheory.Subobject X)
:
↑(CategoryTheory.Abelian.subobjectIsoSubobjectOp X) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op)
(_ :
∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [hf : CategoryTheory.Mono f] [hg : CategoryTheory.Mono g] (i : A ≅ B),
CategoryTheory.CategoryStruct.comp i.hom g = f →
(fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) A f hf = (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) B g hg)
a
@[simp]
theorem
CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(X : C)
(a : (CategoryTheory.Subobject (Opposite.op X))ᵒᵈ)
:
↑(RelIso.symm (CategoryTheory.Abelian.subobjectIsoSubobjectOp X)) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop))
(_ :
∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ Opposite.op X) (g : B ⟶ Opposite.op X) [hf : CategoryTheory.Mono f]
[hg : CategoryTheory.Mono g] (i : A ≅ B),
CategoryTheory.CategoryStruct.comp i.hom g = f →
(fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) A f hf = (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) B g hg)
a
def
CategoryTheory.Abelian.subobjectIsoSubobjectOp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.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.
Instances For
instance
CategoryTheory.Abelian.wellPowered_opposite
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.WellPowered C]
:
A well-powered abelian category is also well-copowered.