# Specific subobjects #

We define equalizerSubobject, kernelSubobject and imageSubobject, which are the subobjects represented by the equalizer, kernel and image of (a pair of) morphism(s) and provide conditions for P.factors f, where P is one of these special subobjects.

TODO: Add conditions for when P is a pullback subobject. TODO: an iff characterisation of (imageSubobject f).Factors h

@[reducible, inline]
abbrev CategoryTheory.Limits.equalizerSubobject {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :

The equalizer of morphisms f g : X ⟶ Y as a Subobject X.

Equations
Instances For
def CategoryTheory.Limits.equalizerSubobjectIso {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
CategoryTheory.Subobject.underlying.obj

The underlying object of equalizerSubobject f g is (up to isomorphism!) the same as the chosen object equalizer f g.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.equalizerSubobject_arrow_assoc {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.Limits.equalizerSubobject_arrow {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
@[simp]
theorem CategoryTheory.Limits.equalizerSubobject_arrow'_assoc {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.Limits.equalizerSubobject_arrow' {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
theorem CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.Limits.equalizerSubobject_arrow_comp {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
theorem CategoryTheory.Limits.equalizerSubobject_factors {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) {W : C} (h : W X) :
.Factors h
theorem CategoryTheory.Limits.equalizerSubobject_factors_iff {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) {W : C} (h : W X) :
@[reducible, inline]
abbrev CategoryTheory.Limits.kernelSubobject {C : Type u} {X : C} {Y : C} (f : X Y) :

The kernel of a morphism f : X ⟶ Y as a Subobject X.

Equations
Instances For
def CategoryTheory.Limits.kernelSubobjectIso {C : Type u} {X : C} {Y : C} (f : X Y) :
CategoryTheory.Subobject.underlying.obj

The underlying object of kernelSubobject f is (up to isomorphism!) the same as the chosen object kernel f.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow_apply {C : Type u} {X : C} {Y : C} (f : X Y) [inst : ] (x : .obj (CategoryTheory.Subobject.underlying.obj )) :
= .arrow x
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow'_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow'_apply {C : Type u} {X : C} {Y : C} (f : X Y) [inst : ] (x : ) :
.arrow () =
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow' {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow_comp_apply {C : Type u} {X : C} {Y : C} (f : X Y) [inst : ] (x : .obj (CategoryTheory.Subobject.underlying.obj )) :
f (.arrow x) = 0 x
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_arrow_comp {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.kernelSubobject_factors {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (h : W X) (w : ) :
.Factors h
theorem CategoryTheory.Limits.kernelSubobject_factors_iff {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (h : W X) :
.Factors h
def CategoryTheory.Limits.factorThruKernelSubobject {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (h : W X) (w : ) :
W CategoryTheory.Subobject.underlying.obj

A factorisation of h : W ⟶ X through kernelSubobject f, assuming h ≫ f = 0.

Equations
• = .factorThru h
Instances For
@[simp]
theorem CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (h : W X) (w : ) :
@[simp]
theorem CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (h : W X) (w : ) :
def CategoryTheory.Limits.kernelSubobjectMap {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) :
CategoryTheory.Subobject.underlying.obj CategoryTheory.Subobject.underlying.obj

A commuting square induces a morphism between the kernel subobjects.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) {Z : C} (h : X' Z) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobjectMap_arrow_apply {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) [inst : ] (x : .obj (CategoryTheory.Subobject.underlying.obj )) :
.arrow = sq.left (.arrow x)
@[simp]
theorem CategoryTheory.Limits.kernelSubobjectMap_arrow {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobjectMap_id {C : Type u} {X : C} {Y : C} {f : X Y} :
= CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj )
@[simp]
theorem CategoryTheory.Limits.kernelSubobjectMap_comp {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} {X'' : C} {Y'' : C} {f'' : X'' Y''} (sq : ) (sq' : ) :
theorem CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) {Z : C} (h : CategoryTheory.Subobject.underlying.obj Z) :
theorem CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) :
theorem CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) {Z : C} (h : ) :
theorem CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map {C : Type u} {X : C} {Y : C} {f : X Y} {X' : C} {Y' : C} {f' : X' Y'} (sq : ) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobject_zero {C : Type u} {A : C} {B : C} :
Equations
• =
theorem CategoryTheory.Limits.le_kernelSubobject {C : Type u} {X : C} {Y : C} (f : X Y) (A : ) (h : = 0) :
def CategoryTheory.Limits.kernelSubobjectIsoComp {C : Type u} {X : C} {Y : C} {X' : C} (f : X' X) (g : X Y) :
CategoryTheory.Subobject.underlying.obj CategoryTheory.Subobject.underlying.obj

The isomorphism between the kernel of f ≫ g and the kernel of g, when f is an isomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow {C : Type u} {X : C} {Y : C} {X' : C} (f : X' X) (g : X Y) :
@[simp]
theorem CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow {C : Type u} {X : C} {Y : C} {X' : C} (f : X' X) (g : X Y) :
theorem CategoryTheory.Limits.kernelSubobject_comp_le {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :

The kernel of f is always a smaller subobject than the kernel of f ≫ h.

@[simp]
theorem CategoryTheory.Limits.kernelSubobject_comp_mono {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :

Postcomposing by a monomorphism does not change the kernel subobject.

instance CategoryTheory.Limits.kernelSubobject_comp_mono_isIso {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.cokernelOrderHom_coe {C : Type u} (X : C) :
∀ (a : ), = CategoryTheory.Subobject.lift (fun (A : C) (f : A X) (x : ) => ) a

Taking cokernels is an order-reversing map from the subobjects of X to the quotient objects of X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.kernelOrderHom_coe {C : Type u} (X : C) :
∀ (a : ), = CategoryTheory.Subobject.lift (fun (A : Cᵒᵖ) (f : A ) (x : ) => ) a

Taking kernels is an order-reversing map from the quotient objects of X to the subobjects of X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.imageSubobject {C : Type u} {X : C} {Y : C} (f : X Y) :

The image of a morphism f g : X ⟶ Y as a Subobject Y.

Equations
Instances For
def CategoryTheory.Limits.imageSubobjectIso {C : Type u} {X : C} {Y : C} (f : X Y) :
CategoryTheory.Subobject.underlying.obj

The underlying object of imageSubobject f is (up to isomorphism!) the same as the chosen object image f.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.imageSubobject_arrow_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.imageSubobject_arrow {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.imageSubobject_arrow'_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.imageSubobject_arrow' {C : Type u} {X : C} {Y : C} (f : X Y) :
def CategoryTheory.Limits.factorThruImageSubobject {C : Type u} {X : C} {Y : C} (f : X Y) :
X CategoryTheory.Subobject.underlying.obj

A factorisation of f : X ⟶ Y through imageSubobject f.

Equations
Instances For
Equations
• =
@[simp]
theorem CategoryTheory.Limits.imageSubobject_arrow_comp_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.imageSubobject_arrow_comp_apply {C : Type u} {X : C} {Y : C} (f : X Y) [inst : ] (x : .obj X) :
= f x
@[simp]
theorem CategoryTheory.Limits.imageSubobject_arrow_comp {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} (h : ) :
theorem CategoryTheory.Limits.imageSubobject_factors_comp_self {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (k : W X) :
.Factors
@[simp]
theorem CategoryTheory.Limits.factorThruImageSubobject_comp_self {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} (k : W X) (h : .Factors ) :
@[simp]
theorem CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {W : C} {W' : C} (k : W W') (k' : W' X) (h : ) :
theorem CategoryTheory.Limits.imageSubobject_comp_le {C : Type u} {X : C} {Y : C} {X' : C} (h : X' X) (f : X Y) :

The image of h ≫ f is always a smaller subobject than the image of f.

@[simp]
theorem CategoryTheory.Limits.imageSubobject_zero_arrow {C : Type u} {X : C} {Y : C} :
.arrow = 0
@[simp]
theorem CategoryTheory.Limits.imageSubobject_zero {C : Type u} {A : C} {B : C} :
instance CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi {C : Type u} {X : C} {Y : C} {X' : C} (h : X' X) (f : X Y) :

The morphism imageSubobject (h ≫ f) ⟶ imageSubobject f is an epimorphism when h is an epimorphism. In general this does not imply that imageSubobject (h ≫ f) = imageSubobject f, although it will when the ambient category is abelian.

Equations
• =
def CategoryTheory.Limits.imageSubobjectCompIso {C : Type u} {X : C} {Y : C} (f : X Y) {Y' : C} (h : Y Y') :
CategoryTheory.Subobject.underlying.obj CategoryTheory.Subobject.underlying.obj

Postcomposing by an isomorphism gives an isomorphism between image subobjects.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Y' : C} (h : Y Y') [] {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow {C : Type u} {X : C} {Y : C} (f : X Y) {Y' : C} (h : Y Y') :
@[simp]
theorem CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Y' : C} (h : Y Y') [] {Z : C} (h : Y' Z) :
@[simp]
theorem CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow {C : Type u} {X : C} {Y : C} (f : X Y) {Y' : C} (h : Y Y') :
theorem CategoryTheory.Limits.imageSubobject_mono {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.imageSubobject_iso_comp {C : Type u} {X : C} {Y : C} {X' : C} (h : X' X) (f : X Y) :

Precomposing by an isomorphism does not change the image subobject.

theorem CategoryTheory.Limits.imageSubobject_le {C : Type u} {A : C} {B : C} {X : } (f : A B) (h : A CategoryTheory.Subobject.underlying.obj X) (w : = f) :
theorem CategoryTheory.Limits.imageSubobject_le_mk {C : Type u} {A : C} {B : C} {X : C} (g : X B) (f : A B) (h : A X) (w : ) :
def CategoryTheory.Limits.imageSubobjectMap {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} (sq : ) :
CategoryTheory.Subobject.underlying.obj CategoryTheory.Subobject.underlying.obj

Given a commutative square between morphisms f and g, we have a morphism in the category from imageSubobject f to imageSubobject g.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.imageSubobjectMap_arrow_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z✝} (sq : ) {Z : C} (h : Z✝ Z) :
@[simp]
theorem CategoryTheory.Limits.imageSubobjectMap_arrow {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} (sq : ) :
theorem CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} (sq : ) :
theorem CategoryTheory.Limits.imageSubobjectIso_comp_image_map {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} (sq : ) :