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
The equalizer of morphisms f g : X ⟶ Y
as a Subobject X
.
Instances For
The underlying object of equalizerSubobject f g
is (up to isomorphism!)
the same as the chosen object equalizer f g
.
Instances For
The kernel of a morphism f : X ⟶ Y
as a Subobject X
.
Instances For
The underlying object of kernelSubobject f
is (up to isomorphism!)
the same as the chosen object kernel f
.
Instances For
A factorisation of h : W ⟶ X
through kernelSubobject f
, assuming h ≫ f = 0
.
Instances For
A commuting square induces a morphism between the kernel subobjects.
Instances For
The isomorphism between the kernel of f ≫ g
and the kernel of g
,
when f
is an isomorphism.
Instances For
The kernel of f
is always a smaller subobject than the kernel of f ≫ h
.
Postcomposing by a 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
.
Instances For
Taking kernels is an order-reversing map from the quotient objects of X
to the subobjects of
X
.
Instances For
The image of a morphism f g : X ⟶ Y
as a Subobject Y
.
Instances For
The underlying object of imageSubobject f
is (up to isomorphism!)
the same as the chosen object image f
.
Instances For
A factorisation of f : X ⟶ Y
through imageSubobject f
.
Instances For
The image of h ≫ f
is always a smaller subobject than the image of f
.
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.
Postcomposing by an isomorphism gives an isomorphism between image subobjects.
Instances For
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 imageSubobject f
to imageSubobject g
.