Structures · Category theory
CategoryTheory.Limits.HasImages
HasImages asserts that every morphism has an image.
- Shape
- One type argument · adds has_image
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CategoryTheory.Limits.HasImages is also a
Concrete types that are instances2
- CategoryTheory.Functor
- CategoryTheory.Sheaf
How is a type an instance?
Loading the hierarchy index…
Assumed by67
- CategoryTheory.Subobject.exists
- CategoryTheory.PreservesImage.iso
- imageToKernel'
- CategoryTheory.Subobject.imageFactorisation
- CategoryTheory.MonoOver.image
- CategoryTheory.PreservesImage.iso_hom
- CategoryTheory.Subobject.sSup
- CategoryTheory.Limits.im
- CategoryTheory.PreservesImage.iso_inv
- CategoryTheory.MonoOver.existsIsoMap
- CategoryTheory.PreservesImage.factorThruImage_comp_hom
- CategoryTheory.Subobject.sup_factors_of_factors_left
- CategoryTheory.PreservesImage.hom_comp_map_image_ι
- imageToKernel'_kernelSubobjectIso
- CategoryTheory.PreservesImage.inv_comp_image_ι_map
- CategoryTheory.MonoOver.exists
- CategoryTheory.Subobject.sup_factors_of_factors_right
- CategoryTheory.Subobject.instCompleteLattice
- CategoryTheory.Limits.hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers
- CategoryTheory.Subobject.exists_iso_map
- CategoryTheory.MonoOver.forgetImage
- CategoryTheory.MonoOver.image_obj
- imageSubobjectIso_imageToKernel'
- CategoryTheory.Limits.HasImages.has_image
- CategoryTheory.MonoOver.supLe
- CategoryTheory.Subobject.existsIsoImage
- imageToKernel_comp_hom_inv_comp
- CategoryTheory.MonoOver.existsPullbackAdj
- imageToKernel_epi_comp
- CategoryTheory.MonoOver.reflective
- CategoryTheory.Limits.im_obj
- CategoryTheory.Subobject.exists.congr_simp
- CategoryTheory.Limits.HasImageMaps.congr_simp
- CategoryTheory.MonoOver.leSupLeft
- CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc
- imageToKernel_comp_right
- CategoryTheory.MonoOver.imageForgetAdj
- imageToKernel_zero_right
- CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc
- CategoryTheory.Subobject.sSup_le
- CategoryTheory.Subobject.existsCompRepresentativeIso
- CategoryTheory.PreservesImage.iso.congr_simp
- CategoryTheory.Subobject.finset_sup_factors
- CategoryTheory.Subobject.imageFactorisation_F_I
- CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc
- CategoryTheory.Subobject.semilatticeSup
- imageToKernel'.congr_simp
- CategoryTheory.Subobject.le_sSup
- CategoryTheory.Subobject.imageFactorisation_F_m
- CategoryTheory.MonoOver.instIsRightAdjointOverForget