Categorical images #
We define the categorical image of f
as a factorisation f = e ≫ m
through a monomorphism m
,
so that m
factors through the m'
in any other such factorisation.
Main definitions #
A
MonoFactorisation
is a factorisationf = e ≫ m
, wherem
is a monomorphismIsImage F
means that a given mono factorisationF
has the universal property of the image.HasImage f
means that there is some image factorization for the morphismf : X ⟶ Y
.HasImages C
means that every morphism inC
has an image.Let
f : X ⟶ Y
andg : P ⟶ Q
be morphisms inC
, which we will represent as objects of the arrow categoryArrow C
. Thensq : f ⟶ g
is a commutative square inC
. Iff
andg
have images, thenHasImageMap sq
represents the fact that there is a morphismi : image f ⟶ image g
making the diagramX ----→ image f ----→ Y | | | | | | ↓ ↓ ↓ P ----→ image g ----→ Q
commute, where the top row is the image factorisation of
f
, the bottom row is the image factorisation ofg
, and the outer rectangle is the commutative squaresq
.If a category
HasImages
, thenHasImageMaps
means that every commutative square admits an image map.If a category
HasImages
, thenHasStrongEpiImages
means that the morphism to the image is always a strong epimorphism.
Main statements #
- When
C
has equalizers, the morphisme
appearing in an image factorisation is an epimorphism. - When
C
has strong epi images, then these images admit image maps.
Future work #
- TODO: coimages, and abelian categories.
- TODO: connect this with existing working in the group theory and ring theory libraries.
A factorisation of a morphism f = e ≫ m
, with m
monic.
- I : C
The obvious factorisation of a monomorphism through itself.
Equations
- CategoryTheory.Limits.MonoFactorisation.self f = { I := X, m := f, m_mono := inst✝, e := CategoryTheory.CategoryStruct.id X, fac := ⋯ }
Equations
The morphism m
in a factorisation f = e ≫ m
through a monomorphism is uniquely
determined.
Any mono factorisation of f
gives a mono factorisation of f ≫ g
when g
is a mono.
A mono factorisation of f ≫ g
, where g
is an isomorphism,
gives a mono factorisation of f
.
Equations
- F.ofCompIso = { I := F.I, m := CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.inv g), m_mono := ⋯, e := F.e, fac := ⋯ }
Any mono factorisation of f
gives a mono factorisation of g ≫ f
.
A mono factorisation of g ≫ f
, where g
is an isomorphism,
gives a mono factorisation of f
.
Equations
- CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F = { I := F.I, m := F.m, m_mono := ⋯, e := CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) F.e, fac := ⋯ }
If f
and g
are isomorphic arrows, then a mono factorisation of f
gives a mono factorisation of g
Equations
- F.ofArrowIso sq = { I := F.I, m := CategoryTheory.CategoryStruct.comp F.m sq.right, m_mono := ⋯, e := CategoryTheory.CategoryStruct.comp (CategoryTheory.inv sq.left) F.e, fac := ⋯ }
Data exhibiting that a given factorisation through a mono is initial.
Data exhibiting that a given factorisation through a mono is initial.
Data exhibiting that a given factorisation through a mono is initial.
The trivial factorisation of a monomorphism satisfies the universal property.
Equations
- CategoryTheory.Limits.IsImage.self f = { lift := fun (F' : CategoryTheory.Limits.MonoFactorisation f) => F'.e, lift_fac := ⋯ }
Equations
Two factorisations through monomorphisms satisfying the universal property must factor through isomorphic objects.
If f
and g
are isomorphic arrows, then a mono factorisation of f
that is an image
gives a mono factorisation of g
that is an image
Equations
- hF.ofArrowIso sq = { lift := fun (F' : CategoryTheory.Limits.MonoFactorisation g.hom) => hF.lift (F'.ofArrowIso (CategoryTheory.inv sq)), lift_fac := ⋯ }
Data exhibiting that a morphism f
has an image.
- F : MonoFactorisation f
Data exhibiting that a morphism
f
has an image. Data exhibiting that a morphism
f
has an image.
Equations
- CategoryTheory.Limits.ImageFactorisation.instInhabitedOfMono f = { default := { F := CategoryTheory.Limits.MonoFactorisation.self f, isImage := CategoryTheory.Limits.IsImage.self f } }
If f
and g
are isomorphic arrows, then an image factorisation of f
gives an image factorisation of g
Equations
- F.ofArrowIso sq = { F := F.F.ofArrowIso sq, isImage := F.isImage.ofArrowIso sq }
HasImage f
means that there exists an image factorisation of f
.
- mk' :: (
- exists_image : Nonempty (ImageFactorisation f)
HasImage f
means that there exists an image factorisation off
. - )
Instances
Some factorisation of f
through a monomorphism (selected with choice).
Equations
The witness of the universal property for the chosen factorisation of f
through
a monomorphism.
Equations
The categorical image of a morphism.
The inclusion of the image of a morphism into the target.
The map from the source to the image of a morphism.
Rewrite in terms of the factorThruImage
interface.
Any other factorisation of the morphism f
through a monomorphism receives a map from the
image.
Equations
If has_image g
, then has_image (f ≫ g)
when f
is an isomorphism.
The image of a monomorphism is isomorphic to the source.
An equation between morphisms gives a comparison map between the images (which momentarily we prove is an iso).
Equations
- One or more equations did not get rendered due to their size.
An equation between morphisms gives an isomorphism between the images.
As long as the category has equalizers,
the image inclusion maps commute with image.eqToIso
.
The comparison map image (f ≫ g) ⟶ image g
.
Equations
- One or more equations did not get rendered due to their size.
image.preComp f g
is a monomorphism.
The two step comparison map
image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h
agrees with the one step comparison map
image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h
.
image.preComp f g
is an epimorphism when f
is an epimorphism
(we need C
to have equalizers to prove this).
image.preComp f g
is an isomorphism when f
is an isomorphism
(we need C
to have equalizers to prove this).
Postcomposing by an isomorphism induces an isomorphism on the image.
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Limits.inhabitedImageMap = { default := { map := CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom), map_ι := ⋯ } }
To give an image map for a commutative square with f
at the top and g
at the bottom, it
suffices to give a map between any mono factorisation of f
and any image factorisation of
g
.
Equations
- One or more equations did not get rendered due to their size.
HasImageMap sq
means that there is an ImageMap
for the square sq
.
- mk' :: (
HasImageMap sq
means that there is anImageMap
for the squaresq
.- )
Instances
Obtain an ImageMap
from a HasImageMap
instance.
Equations
The map on images induced by a commutative square.
Equations
Image maps for composable commutative squares induce an image map in the composite square.
Equations
- CategoryTheory.Limits.imageMapComp sq sq' = { map := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.map sq'), map_ι := ⋯ }
The identity image f ⟶ image f
fits into the commutative square represented by the identity
morphism 𝟙 f
in the arrow category.
Equations
- CategoryTheory.Limits.imageMapId f = { map := CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom), map_ι := ⋯ }
If a category has_image_maps
, then all commutative squares induce morphisms on images.
Instances
The functor from the arrow category of C
to C
itself that maps a morphism to its image
and a commutative square to the induced morphism on images.
Equations
- One or more equations did not get rendered due to their size.
A strong epi-mono factorisation is a decomposition f = e ≫ m
with e
a strong epimorphism
and m
a monomorphism.
- I : C
Satisfying the inhabited linter
Equations
- CategoryTheory.Limits.strongEpiMonoFactorisationInhabited f = { default := { I := Y, m := CategoryTheory.CategoryStruct.id Y, m_mono := ⋯, e := f, fac := ⋯, e_strong_epi := inst✝ } }
A mono factorisation coming from a strong epi-mono factorisation always has the universal property of the image.
Equations
- F.toMonoIsImage = { lift := fun (G : CategoryTheory.Limits.MonoFactorisation f) => ⋯.lift, lift_fac := ⋯ }
A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.
- mk' :: (
A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.
- )
Instances
A category has strong epi images if it has all images and factorThruImage f
is a strong
epimorphism for all f
.
Instances
If there is a single strong epi-mono factorisation of f
, then every image factorisation is a
strong epi-mono factorisation.
If we constructed our images from strong epi-mono factorisations, then these images are strong epi images.
A category with strong epi images has image maps.
If a category has images, equalizers and pullbacks, then images are automatically strong epi images.
If C
has strong epi mono factorisations, then the image is unique up to isomorphism, in that if
f
factors as a strong epi followed by a mono, this factorisation is essentially the image
factorisation.
Equations
- One or more equations did not get rendered due to their size.
A category with strong epi mono factorisations admits functorial epi/mono factorizations.
Equations
- One or more equations did not get rendered due to their size.