# mathlibdocumentation

category_theory.subobject.limits

# Specific subobjects #

We define equalizer_subobject, kernel_subobject and image_subobject, 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 (image_subobject f).factors h

@[reducible]
noncomputable def category_theory.limits.equalizer_subobject {C : Type u} {X Y : C} (f g : X Y)  :

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

noncomputable def category_theory.limits.equalizer_subobject_iso {C : Type u} {X Y : C} (f g : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.equalizer_subobject_arrow_assoc {C : Type u} {X Y : C} (f g : X Y) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.equalizer_subobject_arrow {C : Type u} {X Y : C} (f g : X Y)  :
@[simp]
theorem category_theory.limits.equalizer_subobject_arrow'_assoc {C : Type u} {X Y : C} (f g : X Y) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.equalizer_subobject_arrow' {C : Type u} {X Y : C} (f g : X Y)  :
theorem category_theory.limits.equalizer_subobject_arrow_comp_assoc {C : Type u} {X Y : C} (f g : X Y) {X' : C} (f' : Y X') :
=
theorem category_theory.limits.equalizer_subobject_arrow_comp {C : Type u} {X Y : C} (f g : X Y)  :
theorem category_theory.limits.equalizer_subobject_factors {C : Type u} {X Y : C} (f g : X Y) {W : C} (h : W X) (w : h f = h g) :
theorem category_theory.limits.equalizer_subobject_factors_iff {C : Type u} {X Y : C} (f g : X Y) {W : C} (h : W X) :
h f = h g
@[reducible]
noncomputable def category_theory.limits.kernel_subobject {C : Type u} {X Y : C} (f : X Y)  :

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

noncomputable def category_theory.limits.kernel_subobject_iso {C : Type u} {X Y : C} (f : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.kernel_subobject_arrow_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.kernel_subobject_arrow_apply {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.kernel_subobject_arrow {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.kernel_subobject_arrow'_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.kernel_subobject_arrow'_apply {C : Type u} {X Y : C} (f : X Y) (x : ) :
@[simp]
theorem category_theory.limits.kernel_subobject_arrow' {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.kernel_subobject_arrow_comp_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
= 0 f'
@[simp]
theorem category_theory.limits.kernel_subobject_arrow_comp {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.kernel_subobject_arrow_comp_apply {C : Type u} {X Y : C} (f : X Y)  :
f = 0 x
theorem category_theory.limits.kernel_subobject_factors {C : Type u} {X Y : C} (f : X Y) {W : C} (h : W X) (w : h f = 0) :
theorem category_theory.limits.kernel_subobject_factors_iff {C : Type u} {X Y : C} (f : X Y) {W : C} (h : W X) :
h f = 0
noncomputable def category_theory.limits.factor_thru_kernel_subobject {C : Type u} {X Y : C} (f : X Y) {W : C} (h : W X) (w : h f = 0) :

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

Equations
Instances for category_theory.limits.factor_thru_kernel_subobject
@[simp]
theorem category_theory.limits.factor_thru_kernel_subobject_comp_arrow {C : Type u} {X Y : C} (f : X Y) {W : C} (h : W X) (w : h f = 0) :
@[simp]
theorem category_theory.limits.factor_thru_kernel_subobject_comp_kernel_subobject_iso {C : Type u} {X Y : C} (f : X Y) {W : C} (h : W X) (w : h f = 0) :
noncomputable def category_theory.limits.kernel_subobject_map {C : Type u} {X Y : C} {f : X Y} {X' Y' : C} {f' : X' Y'}  :

A commuting square induces a morphism between the kernel subobjects.

Equations
@[simp]
theorem category_theory.limits.kernel_subobject_map_arrow_assoc {C : Type u} {X Y : C} {f : X Y} {X' Y' : C} {f' : X' Y'} {X'_1 : C} (f'_1 : X' X'_1) :
@[simp]
theorem category_theory.limits.kernel_subobject_map_arrow_apply {C : Type u} {X Y : C} {f : X Y} {X' Y' : C} {f' : X' Y'}  :
= (sq.left)
@[simp]
theorem category_theory.limits.kernel_subobject_map_arrow {C : Type u} {X Y : C} {f : X Y} {X' Y' : C} {f' : X' Y'}  :
@[simp]
theorem category_theory.limits.kernel_subobject_map_id {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.limits.kernel_subobject_map_comp {C : Type u} {X Y : C} {f : X Y} {X' Y' : C} {f' : X' Y'} {X'' Y'' : C} {f'' : X'' Y''} (sq' : ) :
@[simp]
theorem category_theory.limits.kernel_subobject_zero {C : Type u} {A B : C} :
@[protected, instance]
theorem category_theory.limits.le_kernel_subobject {C : Type u} {X Y : C} (f : X Y) (h : A.arrow f = 0) :
noncomputable def category_theory.limits.kernel_subobject_iso_comp {C : Type u} {X Y : C} {X' : C} (f : X' X) (g : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.kernel_subobject_iso_comp_hom_arrow {C : Type u} {X Y : C} {X' : C} (f : X' X) (g : X Y)  :
@[simp]
theorem category_theory.limits.kernel_subobject_iso_comp_inv_arrow {C : Type u} {X Y : C} {X' : C} (f : X' X) (g : X Y)  :
theorem category_theory.limits.kernel_subobject_comp_le {C : Type u} {X 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 category_theory.limits.kernel_subobject_comp_mono {C : Type u} {X Y : C} (f : X Y) {Z : C} (h : Y Z)  :

Postcomposing by an monomorphism does not change the kernel subobject.

@[protected, instance]
def category_theory.limits.kernel_subobject_comp_mono_is_iso {C : Type u} {X Y : C} (f : X Y) {Z : C} (h : Y Z)  :
noncomputable def category_theory.limits.cokernel_order_hom {C : Type u} (X : C) :

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

Equations
@[simp]
theorem category_theory.limits.cokernel_order_hom_coe {C : Type u} (X : C)  :
= category_theory.subobject.lift (λ (A : C) (f : A X) (hf : , _
noncomputable def category_theory.limits.kernel_order_hom {C : Type u} (X : C) :

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

Equations
@[simp]
theorem category_theory.limits.kernel_order_hom_coe {C : Type u} (X : C) (ᾰ : category_theory.subobject (opposite.op X)) :
= category_theory.subobject.lift (λ (A : Cᵒᵖ) (f : A (hf : , _
@[reducible]
noncomputable def category_theory.limits.image_subobject {C : Type u} {X Y : C} (f : X Y)  :

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

noncomputable def category_theory.limits.image_subobject_iso {C : Type u} {X Y : C} (f : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.image_subobject_arrow_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.image_subobject_arrow {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.image_subobject_arrow'_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.image_subobject_arrow' {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.factor_thru_image_subobject {C : Type u} {X Y : C} (f : X Y)  :

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

Equations
Instances for category_theory.limits.factor_thru_image_subobject
@[protected, instance]
@[simp]
theorem category_theory.limits.image_subobject_arrow_comp {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.image_subobject_arrow_comp_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.image_subobject_arrow_comp_apply {C : Type u} {X Y : C} (f : X Y) (x : X) :
theorem category_theory.limits.image_subobject_arrow_comp_eq_zero {C : Type u} {X Y Z : C} {f : X Y} {g : Y Z} (h : f g = 0) :
theorem category_theory.limits.image_subobject_factors_comp_self {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) :
@[simp]
theorem category_theory.limits.factor_thru_image_subobject_comp_self {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) (h : (k f)) :
@[simp]
theorem category_theory.limits.factor_thru_image_subobject_comp_self_assoc {C : Type u} {X Y : C} (f : X Y) {W W' : C} (k : W W') (k' : W' X) (h : (k k' f)) :
(k k' f) h =
theorem category_theory.limits.image_subobject_comp_le {C : Type u} {X Y 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 category_theory.limits.image_subobject_zero_arrow {C : Type u} {X Y : C}  :
@[simp]
@[protected, instance]
def category_theory.limits.image_subobject_comp_le_epi_of_epi {C : Type u} {X Y : C} {X' : C} (h : X' X) (f : X Y)  :

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

noncomputable def category_theory.limits.image_subobject_comp_iso {C : Type u} {X Y : C} (f : X Y) {Y' : C} (h : Y Y')  :

Postcomposing by an isomorphism gives an isomorphism between image subobjects.

Equations
@[simp]
theorem category_theory.limits.image_subobject_comp_iso_hom_arrow_assoc {C : Type u} {X Y : C} (f : X Y) {Y' : C} (h : Y Y') {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.image_subobject_comp_iso_hom_arrow {C : Type u} {X Y : C} (f : X Y) {Y' : C} (h : Y Y')  :
@[simp]
theorem category_theory.limits.image_subobject_comp_iso_inv_arrow {C : Type u} {X Y : C} (f : X Y) {Y' : C} (h : Y Y')  :
@[simp]
theorem category_theory.limits.image_subobject_comp_iso_inv_arrow_assoc {C : Type u} {X Y : C} (f : X Y) {Y' : C} (h : Y Y') {X' : C} (f' : Y' X') :
theorem category_theory.limits.image_subobject_mono {C : Type u} {X Y : C} (f : X Y)  :
theorem category_theory.limits.image_subobject_iso_comp {C : Type u} {X Y : C} {X' : C} (h : X' X) (f : X Y)  :

Precomposing by an isomorphism does not change the image subobject.

theorem category_theory.limits.image_subobject_le {C : Type u} {A B : C} (f : A B) (h : A X) (w : h X.arrow = f) :
theorem category_theory.limits.image_subobject_le_mk {C : Type u} {A B X : C} (g : X B) (f : A B) (h : A X) (w : h g = f) :
noncomputable def category_theory.limits.image_subobject_map {C : Type u} {W X Y Z : C} {f : W X} {g : Y Z}  :

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

Equations
@[simp]
theorem category_theory.limits.image_subobject_map_arrow {C : Type u} {W X Y Z : C} {f : W X} {g : Y Z}  :
@[simp]
theorem category_theory.limits.image_subobject_map_arrow_assoc {C : Type u} {W X Y Z : C} {f : W X} {g : Y Z} {X' : C} (f' : Z X') :