Documentation

Mathlib.CategoryTheory.Abelian.Subobject

Equivalence between subobjects and quotients in an abelian category #

source
@[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
source
@[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
source
def CategoryTheory.Abelian.subobjectIsoSubobjectOp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) :
CategoryTheory.Subobject X ≃o (CategoryTheory.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.

Instances For
    source
    instance CategoryTheory.Abelian.wellPowered_opposite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.WellPowered C] :
    CategoryTheory.WellPowered Cᵒᵖ

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