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
The equalizer of morphisms f g : X ⟶ Y
as a subobject X
.
The underlying object of equalizer_subobject f g
is (up to isomorphism!)
the same as the chosen object equalizer f g
.
The kernel of a morphism f : X ⟶ Y
as a subobject X
.
The underlying object of kernel_subobject f
is (up to isomorphism!)
the same as the chosen object kernel f
.
A factorisation of h : W ⟶ X
through kernel_subobject f
, assuming h ≫ f = 0
.
Equations
Instances for category_theory.limits.factor_thru_kernel_subobject
A commuting square induces a morphism between the kernel subobjects.
Equations
The isomorphism between the kernel of f ≫ g
and the kernel of g
,
when f
is an isomorphism.
The kernel of f
is always a smaller subobject than the kernel of f ≫ h
.
Postcomposing by an monomorphism does not change the kernel subobject.
Taking cokernels is an order-reversing map from the subobjects of X
to the quotient objects
of X
.
Equations
- category_theory.limits.cokernel_order_hom X = {to_fun := category_theory.subobject.lift (λ (A : C) (f : A ⟶ X) (hf : category_theory.mono f), category_theory.subobject.mk (category_theory.limits.cokernel.π f).op) _, monotone' := _}
Taking kernels is an order-reversing map from the quotient objects of X
to the subobjects of
X
.
Equations
- category_theory.limits.kernel_order_hom X = {to_fun := 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)) _, monotone' := _}
The image of a morphism f g : X ⟶ Y
as a subobject Y
.
The underlying object of image_subobject f
is (up to isomorphism!)
the same as the chosen object image f
.
A factorisation of f : X ⟶ Y
through image_subobject f
.
Equations
Instances for category_theory.limits.factor_thru_image_subobject
The image of h ≫ f
is always a smaller subobject than the image of f
.
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.
Postcomposing by an isomorphism gives an isomorphism between image subobjects.
Precomposing by an isomorphism does not change the image subobject.
Given a commutative square between morphisms f
and g
,
we have a morphism in the category from image_subobject f
to image_subobject g
.