Images

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Images.lean

Statistics

Metric	Count
Definitions HasImage, HasImageMap, imageMap, HasImageMaps, HasImages, HasStrongEpiImages, HasStrongEpiMonoFactorisations, imageFactorisation, isImage, monoFactorisation, ImageFactorisation, F, copy, instInhabitedOfMono, isImage, ofArrowIso, ofIsoI, ImageMap, map, transport, copy, instInhabitedSelf, isoExt, ofArrowIso, ofIsoI, self, MonoFactorisation, I, compMono, copy, e, instInhabitedOfMono, isoComp, m, ofArrowIso, ofCompIso, ofIsoComp, ofIsoI, self, StrongEpiMonoFactorisation, toMonoFactorisation, toMonoIsImage, factorThruImage, functorialEpiMonoFactorizationData, im, image, compIso, eqToHom, eqToIso, isoStrongEpiMono, map, preComp, ι, imageMapComp, imageMapId, imageMonoIsoSource, inhabitedImageMap, strongEpiMonoFactorisationInhabited	58
Theorems hasStrongEpiMonoFactorisations_imp_of_isEquivalence, exists_image, mk, of_arrow_iso, uniq, comp, has_image_map, mk, transport, has_image_map, has_image, strong_factorThruImage, has_fac, mk, copy_F, copy_isImage, ofArrowIso_F, ofArrowIso_isImage, ofIsoI_F, ofIsoI_isImage, ext, ext_iff, factor_map, factor_map_assoc, map_uniq, map_uniq_aux, map_ι, map_ι_assoc, injEq', copy_lift, e_isoExt_hom, e_isoExt_inv, fac_lift, fac_lift_assoc, isoExt_hom, isoExt_hom_m, isoExt_inv, isoExt_inv_m, lift_fac, lift_fac_assoc, lift_ι, lift_ι_assoc, ofArrowIso_lift, ofIsoI_lift, self_lift, compMono_I, compMono_e, compMono_m, copy_I, copy_e, copy_m, ext, fac, fac_apply, fac_assoc, isoComp_I, isoComp_e, isoComp_m, m_mono, ofArrowIso_I, ofArrowIso_e, ofArrowIso_m, ofCompIso_I, ofCompIso_e, ofCompIso_m, ofIsoComp_I, ofIsoComp_e, ofIsoComp_m, ofIsoI_I, ofIsoI_e, ofIsoI_m, e_strong_epi, as_factorThruImage, epi_image_of_epi, epi_of_epi_image, hasImageMapOfIsIso, hasImageMapsOfHasStrongEpiImages, hasImage_comp_iso, hasImage_iso_comp, hasImages_of_hasStrongEpiMonoFactorisations, hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers, hasStrongEpiImages_of_hasStrongEpiMonoFactorisations, im_map, im_obj, as_ι, compIso_hom_comp_image_ι, compIso_hom_comp_image_ι_assoc, compIso_inv_comp_image_ι, compIso_inv_comp_image_ι_assoc, eq_fac, ext, fac, fac_assoc, fac_lift, fac_lift_assoc, factorThruImage_preComp, factorThruImage_preComp_assoc, factor_map, isImage_lift, isIso_precomp_iso, isoStrongEpiMono_hom_comp_ι, isoStrongEpiMono_inv_comp_mono, lift_fac, lift_fac_assoc, lift_mk_comp, lift_mk_comp_assoc, lift_mk_factorThruImage, lift_mk_factorThruImage_assoc, lift_mono, map_comp, map_homMk'_ι, map_id, map_ι, preComp_comp, preComp_epi_of_epi, preComp_mono, preComp_ι, preComp_ι_assoc, imageMonoIsoSource_hom_self, imageMonoIsoSource_hom_self_assoc, imageMonoIsoSource_inv_ι, imageMonoIsoSource_inv_ι_assoc, instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair, instHasImageCompOfIsIso, instHasImageHomMk, instIsIsoEqToHom, instMonoι, instSubsingletonImageMap, mono_hasImage, strongEpi_factorThruImage_of_strongEpiMonoFactorisation, strongEpi_of_strongEpiMonoFactorisation	131
Total	189

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasStrongEpiMonoFactorisations_imp_of_isEquivalence 📖	mathematical	—	CategoryTheory.Limits.HasStrongEpiMonoFactorisations	—	CategoryTheory.Limits.HasStrongEpiMonoFactorisations.has_fac CategoryTheory.mono_comp map_mono preservesMonomorphisms_of_isRightAdjoint isRightAdjoint_of_isEquivalence CategoryTheory.Limits.MonoFactorisation.m_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Category.assoc map_comp_assoc CategoryTheory.Limits.MonoFactorisation.fac fun_inv_map CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.strongEpi_comp CategoryTheory.strongEpi_of_isIso CategoryTheory.NatIso.inv_app_isIso CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasImage 📖	CompData	10 math math: HasImage.of_arrow_iso, HasImages.has_image, mono_hasImage, hasImage_iso_comp, instHasImageHomMk, instHasImageCompOfIsIso, Types.instHasImage, HasImage.mk, hasImage_comp_iso, hasImage_zero
HasImageMap 📖	CompData	5 math math: HasImageMaps.has_image_map, hasImageMapOfIsIso, HasImageMap.transport, HasImageMap.mk, HasImageMap.comp
HasImageMaps 📖	CompData	2 math math: hasImageMapsOfHasStrongEpiImages, Types.instHasImageMapsType
HasImages 📖	CompData	5 math math: CategoryTheory.FunctorToTypes.instHasImagesFunctorType, Types.instHasImagesType, CategoryTheory.instHasImagesSheafType, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages, hasImages_of_hasStrongEpiMonoFactorisations
HasStrongEpiImages 📖	CompData	3 math math: hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers, SimplexCategory.instHasStrongEpiImages, hasStrongEpiImages_of_hasStrongEpiMonoFactorisations
HasStrongEpiMonoFactorisations 📖	CompData	7 math math: CategoryTheory.FunctorToTypes.instHasStrongEpiMonoFactorisationsFunctorType, CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence, CategoryTheory.Regular.hasStrongEpiMonoFactorisations, HasStrongEpiMonoFactorisations.mk, SimplexCategory.instHasStrongEpiMonoFactorisations, NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations, CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations
ImageFactorisation 📖	CompData	1 math math: HasImage.exists_image
ImageMap 📖	CompData	2 math math: HasImageMap.has_image_map, instSubsingletonImageMap
MonoFactorisation 📖	CompData	—
StrongEpiMonoFactorisation 📖	CompData	1 math math: HasStrongEpiMonoFactorisations.has_fac
factorThruImage 📖	CompOp	35 math math: as_factorThruImage, CategoryTheory.PreservesImage.factorThruImage_comp_hom, imageToKernel_unop, image.lift_mk_factorThruImage, imageToKernel_op, kernelFactorThruImage_hom_comp_ι_assoc, CategoryTheory.image_ι_op_comp_imageUnopOp_hom, image.fac_lift, CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc, image.factorThruImage_preComp, HasStrongEpiImages.strong_factorThruImage, CategoryTheory.PreservesImage.iso_hom, CategoryTheory.MonoOver.image_map, ImageMap.factor_map_assoc, image.fac_lift_assoc, CategoryTheory.factorThruImage_comp_imageUnopOp_inv, image.fac, ImageMap.factor_map, CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv, instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair, image.factorThruImage_preComp_assoc, kernelFactorThruImage_inv_comp_ι, CategoryTheory.imageUnopOp_hom_comp_image_ι, CategoryTheory.Abelian.coimageIsoImage'_hom, image.fac_assoc, strongEpi_factorThruImage_of_strongEpiMonoFactorisation, comp_factorThruImage_eq_zero, image.lift_mk_factorThruImage_assoc, SimplexCategory.factorThruImage_eq, kernelFactorThruImage_hom_comp_ι, CategoryTheory.PreservesImage.iso_inv, kernelFactorThruImage_inv_comp_ι_assoc, CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage, SimplexCategory.instEpiFactorThruImage, image.factor_map
functorialEpiMonoFactorizationData 📖	CompOp	—
im 📖	CompOp	2 math math: im_map, im_obj
image 📖	CompOp	99 math math: imageSubobject_arrow_assoc, image.isIso_precomp_iso, cokernelImageι_inv, CategoryTheory.PreservesImage.factorThruImage_comp_hom, imageToKernel_unop, image.compIso_hom_comp_image_ι, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', image.compIso_hom_comp_image_ι_assoc, imageToKernel'_kernelSubobjectIso, image.lift_mk_factorThruImage, image.map_id, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel', image.eq_fac, image.map_comp, imageToKernel_op, image.lift_fac_assoc, kernelFactorThruImage_hom_comp_ι_assoc, image.isoStrongEpiMono_hom_comp_ι, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι, CategoryTheory.image_ι_op_comp_imageUnopOp_hom, image.preComp_epi_of_epi, image.fac_lift, image.map_ι, ModuleCat.imageIsoRange_hom_subtype, ModuleCat.imageIsoRange_inv_image_ι_apply, CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc, imageMonoIsoSource_hom_self, image.factorThruImage_preComp, HasStrongEpiImages.strong_factorThruImage, CategoryTheory.PreservesImage.iso_hom, CategoryTheory.MonoOver.image_map, ImageMap.factor_map_assoc, image.ι_zero, image.lift_mono, image.fac_lift_assoc, image.map_homMk'_ι, CategoryTheory.PreservesImage.hom_comp_map_image_ι, imageSubobjectIso_comp_image_map, CategoryTheory.factorThruImage_comp_imageUnopOp_inv, image.isoStrongEpiMono_inv_comp_mono, CategoryTheory.PreservesImage.inv_comp_image_ι_map, CategoryTheory.Abelian.imageIsoImage_inv, image.lift_fac, imageMonoIsoSource_inv_ι, image.fac, ModuleCat.imageIsoRange_hom_subtype_assoc, image.preComp_ι, ImageMap.factor_map, CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv, SimplexCategory.image_eq, ModuleCat.imageIsoRange_inv_image_ι, image.factorThruImage_preComp_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, im_obj, instMonoι, ModuleCat.imageIsoRange_inv_image_ι_assoc, imageSubobjectIso_imageToKernel', imageSubobject_arrow, instIsIsoEqToHom, ImageMap.map_ι, kernelFactorThruImage_inv_comp_ι, image.preComp_mono, imageSubobject_arrow'_assoc, image.preComp_comp, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι, CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι, CategoryTheory.imageUnopOp_hom_comp_image_ι, image_ι_comp_eq_zero, CategoryTheory.Abelian.coimageIsoImage'_hom, image.fac_assoc, CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc, strongEpi_factorThruImage_of_strongEpiMonoFactorisation, image.ι_zero', epi_image_of_epi, imageMonoIsoSource_inv_ι_assoc, image_map_comp_imageSubobjectIso_inv, comp_factorThruImage_eq_zero, image.lift_mk_factorThruImage_assoc, ImageMap.map_ι_assoc, image.compIso_inv_comp_image_ι_assoc, image.preComp_ι_assoc, kernelFactorThruImage_hom_comp_ι, CategoryTheory.PreservesImage.iso_inv, kernelFactorThruImage_inv_comp_ι_assoc, imageMonoIsoSource_hom_self_assoc, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel', CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', SimplexCategory.instEpiFactorThruImage, ModuleCat.imageIsoRange_hom_subtype_apply, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel', image.factor_map, imageSubobject_arrow', CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc, CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc, cokernelImageι_hom, image.compIso_inv_comp_image_ι
imageMapComp 📖	CompOp	—
imageMapId 📖	CompOp	—
imageMonoIsoSource 📖	CompOp	4 math math: imageMonoIsoSource_hom_self, imageMonoIsoSource_inv_ι, imageMonoIsoSource_inv_ι_assoc, imageMonoIsoSource_hom_self_assoc
inhabitedImageMap 📖	CompOp	—
strongEpiMonoFactorisationInhabited 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
as_factorThruImage 📖	mathematical	—	MonoFactorisation.e Image.monoFactorisation factorThruImage	—	—
epi_image_of_epi 📖	mathematical	—	CategoryTheory.Epi image image.ι	—	CategoryTheory.epi_of_epi image.fac
epi_of_epi_image 📖	mathematical	—	CategoryTheory.Epi	—	image.fac CategoryTheory.epi_comp
hasImageMapOfIsIso 📖	mathematical	—	HasImageMap	—	CategoryTheory.IsIso.inv_isIso CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Arrow.isIso_right CategoryTheory.Category.assoc MonoFactorisation.ofArrowIso_m image.lift_fac CategoryTheory.Comma.comp_right CategoryTheory.IsIso.hom_inv_id CategoryTheory.Comma.id_right CategoryTheory.Category.comp_id
hasImageMapsOfHasStrongEpiImages 📖	mathematical	—	HasImageMaps	—	HasImages.has_image CategoryTheory.Category.assoc image.fac CategoryTheory.Arrow.w_mk_right image.fac_assoc CategoryTheory.sq_hasLift_of_hasLiftingProperty CategoryTheory.StrongEpi.llp HasStrongEpiImages.strong_factorThruImage instMonoι CategoryTheory.CommSq.fac_right
hasImage_comp_iso 📖	mathematical	—	HasImage CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Category.comp_id CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.assoc image.lift_fac image.as_ι
hasImage_iso_comp 📖	mathematical	—	HasImage CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	image.lift_fac
hasImages_of_hasStrongEpiMonoFactorisations 📖	mathematical	—	HasImages	—	HasStrongEpiMonoFactorisations.has_fac
hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers 📖	mathematical	—	HasStrongEpiImages	—	CategoryTheory.StrongEpi.mk' HasImages.has_image instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair hasLimitOfHasLimitsOfShape CategoryTheory.CommSq.HasLift.mk' CategoryTheory.mono_comp pullback.snd_of_mono instMonoι CategoryTheory.CommSq.w limit.lift_π_assoc image.fac image.fac_lift_assoc pullback.lift_fst image.ext CategoryTheory.Category.assoc pullback.lift_fst_assoc
hasStrongEpiImages_of_hasStrongEpiMonoFactorisations 📖	mathematical	—	HasStrongEpiImages hasImages_of_hasStrongEpiMonoFactorisations	—	hasImages_of_hasStrongEpiMonoFactorisations strongEpi_factorThruImage_of_strongEpiMonoFactorisation HasImages.has_image HasStrongEpiMonoFactorisations.has_fac
im_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow im image.map HasImageMaps.has_image_map	—	—
im_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow im image CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
imageMonoIsoSource_hom_self 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image mono_hasImage CategoryTheory.Iso.hom imageMonoIsoSource image.ι	—	mono_hasImage imageMonoIsoSource_inv_ι CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp
imageMonoIsoSource_hom_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image mono_hasImage CategoryTheory.Iso.hom imageMonoIsoSource image.ι	—	mono_hasImage CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageMonoIsoSource_hom_self
imageMonoIsoSource_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image mono_hasImage CategoryTheory.Iso.inv imageMonoIsoSource image.ι	—	mono_hasImage image.fac
imageMonoIsoSource_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image mono_hasImage CategoryTheory.Iso.inv imageMonoIsoSource image.ι	—	mono_hasImage CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageMonoIsoSource_inv_ι
instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair 📖	mathematical	HasLimit WalkingParallelPair walkingParallelPairHomCategory parallelPair image	CategoryTheory.Epi factorThruImage	—	image.ext
instHasImageCompOfIsIso 📖	mathematical	—	HasImage CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	instMonoι CategoryTheory.Category.assoc image.fac MonoFactorisation.m_mono MonoFactorisation.fac CategoryTheory.IsIso.inv_hom_id_assoc image.lift_fac
instHasImageHomMk 📖	mathematical	—	HasImage CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
instIsIsoEqToHom 📖	mathematical	—	CategoryTheory.IsIso image image.eqToHom	—	CategoryTheory.cancel_mono instMonoι CategoryTheory.Category.assoc image.lift_mk_factorThruImage CategoryTheory.Category.id_comp
instMonoι 📖	mathematical	—	CategoryTheory.Mono image image.ι	—	MonoFactorisation.m_mono
instSubsingletonImageMap 📖	mathematical	—	ImageMap	—	ImageMap.ext ImageMap.map_uniq
mono_hasImage 📖	mathematical	—	HasImage	—	—
strongEpi_factorThruImage_of_strongEpiMonoFactorisation 📖	mathematical	—	CategoryTheory.StrongEpi image factorThruImage	—	strongEpi_of_strongEpiMonoFactorisation
strongEpi_of_strongEpiMonoFactorisation 📖	mathematical	—	CategoryTheory.StrongEpi MonoFactorisation.I MonoFactorisation.e	—	IsImage.e_isoExt_hom CategoryTheory.strongEpi_comp StrongEpiMonoFactorisation.e_strong_epi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom

CategoryTheory.Limits.HasImage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_image 📖	mathematical	—	CategoryTheory.Limits.ImageFactorisation	—	—
mk 📖	mathematical	—	CategoryTheory.Limits.HasImage	—	—
of_arrow_iso 📖	mathematical	—	CategoryTheory.Limits.HasImage CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	exists_image
uniq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Limits.image.ι	CategoryTheory.Limits.image.lift	—	CategoryTheory.cancel_mono CategoryTheory.Limits.MonoFactorisation.m_mono CategoryTheory.Limits.image.lift_fac

CategoryTheory.Limits.HasImageMap

Definitions

Name	Category	Theorems
imageMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	CategoryTheory.Limits.HasImageMap CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow	—	CategoryTheory.Category.assoc CategoryTheory.Limits.ImageMap.map_ι CategoryTheory.Limits.ImageMap.map_ι_assoc CategoryTheory.Comma.comp_right
has_image_map 📖	mathematical	—	CategoryTheory.Limits.ImageMap	—	—
mk 📖	mathematical	—	CategoryTheory.Limits.HasImageMap	—	—
transport 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.CommaMorphism.right	CategoryTheory.Limits.HasImageMap	—	—

CategoryTheory.Limits.HasImageMaps

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_image_map 📖	mathematical	—	CategoryTheory.Limits.HasImageMap CategoryTheory.Limits.HasImages.has_image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—

CategoryTheory.Limits.HasImages

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_image 📖	mathematical	—	CategoryTheory.Limits.HasImage	—	—

CategoryTheory.Limits.HasStrongEpiImages

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strong_factorThruImage 📖	mathematical	—	CategoryTheory.StrongEpi CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.factorThruImage	—	—

CategoryTheory.Limits.HasStrongEpiMonoFactorisations

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_fac 📖	mathematical	—	CategoryTheory.Limits.StrongEpiMonoFactorisation	—	—
mk 📖	mathematical	—	CategoryTheory.Limits.HasStrongEpiMonoFactorisations	—	—

CategoryTheory.Limits.Image

Definitions

Name	Category	Theorems
imageFactorisation 📖	CompOp	—
isImage 📖	CompOp	1 math math: CategoryTheory.Limits.image.isImage_lift
monoFactorisation 📖	CompOp	6 math math: CategoryTheory.Limits.as_factorThruImage, CategoryTheory.Limits.IsImage.lift_ι_assoc, CategoryTheory.Limits.image.isImage_lift, CategoryTheory.Limits.IsImage.lift_ι, CategoryTheory.Limits.image.as_ι, CategoryTheory.PreservesImage.iso_inv

CategoryTheory.Limits.ImageFactorisation

Definitions

Name	Category	Theorems
F 📖	CompOp	7 math math: CategoryTheory.Subobject.imageFactorisation_F_m, ofIsoI_F, ofArrowIso_F, ofIsoI_isImage, CategoryTheory.Subobject.imageFactorisation_F_I, CategoryTheory.Regular.frobeniusMorphism_isPullback, ofArrowIso_isImage
copy 📖	CompOp	2 math math: copy_F, copy_isImage
instInhabitedOfMono 📖	CompOp	—
isImage 📖	CompOp	3 math math: ofIsoI_isImage, ofArrowIso_isImage, copy_isImage
ofArrowIso 📖	CompOp	2 math math: ofArrowIso_F, ofArrowIso_isImage
ofIsoI 📖	CompOp	2 math math: ofIsoI_F, ofIsoI_isImage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
copy_F 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I F CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Limits.MonoFactorisation.e	copy CategoryTheory.Limits.MonoFactorisation.copy	—	—
copy_isImage 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I F CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Limits.MonoFactorisation.e	isImage copy CategoryTheory.Limits.IsImage.copy	—	—
ofArrowIso_F 📖	mathematical	—	F CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom ofArrowIso CategoryTheory.Limits.MonoFactorisation.ofArrowIso	—	—
ofArrowIso_isImage 📖	mathematical	—	isImage CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom ofArrowIso CategoryTheory.Limits.IsImage.ofArrowIso F	—	—
ofIsoI_F 📖	mathematical	—	F ofIsoI CategoryTheory.Limits.MonoFactorisation.ofIsoI	—	—
ofIsoI_isImage 📖	mathematical	—	isImage ofIsoI CategoryTheory.Limits.IsImage.ofIsoI F	—	—

CategoryTheory.Limits.ImageMap

Definitions

Name	Category	Theorems
map 📖	CompOp	6 math math: factor_map_assoc, factor_map, ext_iff, map_ι, map_ι_assoc, map_uniq
transport 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	map	—	—	—
ext_iff 📖	mathematical	—	map	—	ext
factor_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Limits.image CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.factorThruImage map CategoryTheory.CommaMorphism.left	—	CategoryTheory.cancel_mono CategoryTheory.Limits.instMonoι CategoryTheory.Category.assoc map_ι CategoryTheory.Limits.image.fac_assoc CategoryTheory.Limits.image.fac CategoryTheory.Arrow.w_mk_right
factor_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Limits.image CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.factorThruImage map CategoryTheory.CommaMorphism.left	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factor_map
map_uniq 📖	mathematical	—	map	—	map_uniq_aux map_ι
map_uniq_aux 📖	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.image.ι CategoryTheory.CommaMorphism.right	—	—	CategoryTheory.cancel_mono CategoryTheory.Limits.instMonoι
map_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom map CategoryTheory.Limits.image.ι CategoryTheory.CommaMorphism.right	—	—
map_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom map CategoryTheory.Limits.image.ι CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_ι

CategoryTheory.Limits.ImageMap.mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injEq' 📖	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.image.ι CategoryTheory.CommaMorphism.right	—	—	CategoryTheory.Limits.ImageMap.map_uniq_aux

CategoryTheory.Limits.IsImage

Definitions

Name	Category	Theorems
copy 📖	CompOp	2 math math: CategoryTheory.Limits.ImageFactorisation.copy_isImage, copy_lift
instInhabitedSelf 📖	CompOp	—
isoExt 📖	CompOp	6 math math: e_isoExt_inv, isoExt_inv_m, isoExt_hom_m, e_isoExt_hom, isoExt_hom, isoExt_inv
ofArrowIso 📖	CompOp	2 math math: ofArrowIso_lift, CategoryTheory.Limits.ImageFactorisation.ofArrowIso_isImage
ofIsoI 📖	CompOp	2 math math: ofIsoI_lift, CategoryTheory.Limits.ImageFactorisation.ofIsoI_isImage
self 📖	CompOp	1 math math: self_lift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
copy_lift 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Limits.MonoFactorisation.e	lift CategoryTheory.Limits.MonoFactorisation.copy copy	—	—
e_isoExt_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.MonoFactorisation.e CategoryTheory.Iso.hom isoExt	—	fac_lift
e_isoExt_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.MonoFactorisation.e CategoryTheory.Iso.inv isoExt	—	fac_lift
fac_lift 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.MonoFactorisation.e lift	—	CategoryTheory.cancel_mono CategoryTheory.Limits.MonoFactorisation.m_mono CategoryTheory.Category.assoc lift_fac CategoryTheory.Limits.MonoFactorisation.fac
fac_lift_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.MonoFactorisation.e lift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac_lift
isoExt_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.MonoFactorisation.I isoExt lift	—	—
isoExt_hom_m 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Iso.hom isoExt CategoryTheory.Limits.MonoFactorisation.m	—	lift_fac
isoExt_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.MonoFactorisation.I isoExt lift	—	—
isoExt_inv_m 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Iso.inv isoExt CategoryTheory.Limits.MonoFactorisation.m	—	lift_fac
lift_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I lift CategoryTheory.Limits.MonoFactorisation.m	—	—
lift_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I lift CategoryTheory.Limits.MonoFactorisation.m	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fac
lift_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.Image.monoFactorisation lift CategoryTheory.Limits.image.ι CategoryTheory.Limits.MonoFactorisation.m	—	lift_fac
lift_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.Image.monoFactorisation lift CategoryTheory.Limits.image.ι CategoryTheory.Limits.MonoFactorisation.m	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_ι
ofArrowIso_lift 📖	mathematical	—	lift CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.MonoFactorisation.ofArrowIso ofArrowIso CategoryTheory.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
ofIsoI_lift 📖	mathematical	—	lift CategoryTheory.Limits.MonoFactorisation.ofIsoI ofIsoI CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Iso.inv	—	—
self_lift 📖	mathematical	—	lift CategoryTheory.Limits.MonoFactorisation.self self CategoryTheory.Limits.MonoFactorisation.e	—	—

CategoryTheory.Limits.MonoFactorisation

Definitions

Name	Category	Theorems
I 📖	CompOp	55 math math: fac, CategoryTheory.Limits.IsImage.e_isoExt_inv, AddCommGrpCat.image.lift_fac, ofArrowIso_e, CategoryTheory.Limits.monoFactorisationZero_I, CategoryTheory.Limits.IsImage.lift_ι_assoc, compMono_m, CategoryTheory.Limits.IsImage.lift_fac, CategoryTheory.Limits.image.lift_mk_factorThruImage, m_mono, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_I, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, CategoryTheory.Limits.image.lift_fac_assoc, compMono_I, CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation, CategoryTheory.Limits.image.fac_lift, isoComp_e, fac_assoc, CategoryTheory.Limits.IsImage.ofIsoI_lift, CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi, ModuleCat.image.lift_fac, CategoryTheory.Limits.IsImage.isoExt_inv_m, CategoryTheory.Limits.image.lift_mono, CategoryTheory.Limits.image.fac_lift_assoc, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_I, CategoryTheory.Limits.image.lift_fac, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison, CategoryTheory.Limits.IsImage.isoExt_hom_m, ofCompIso_m, ofIsoComp_e, CategoryTheory.Limits.IsImage.e_isoExt_hom, CategoryTheory.Limits.IsImage.isoExt_hom, ofIsoI_I, ofCompIso_I, ofArrowIso_m, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi, CategoryTheory.Subobject.imageFactorisation_F_I, ofIsoI_m, CategoryTheory.Limits.IsImage.lift_fac_assoc, ofArrowIso_I, kernel_ι_comp, ofIsoComp_I, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.Limits.IsImage.lift_ι, ofIsoI_e, CategoryTheory.Limits.IsImage.fac_lift, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_I, CategoryTheory.Limits.IsImage.isoExt_inv, CategoryTheory.FunctorToTypes.monoFactorisation_I, fac_apply, CategoryTheory.Limits.image.lift_mk_comp, CategoryTheory.Regular.instIsRegularEpiEStrongEpiMonoFactorisation, CategoryTheory.Limits.IsImage.fac_lift_assoc, CategoryTheory.Limits.Types.Image.lift_fac, isoComp_I
compMono 📖	CompOp	3 math math: compMono_m, compMono_I, compMono_e
copy 📖	CompOp	5 math math: copy_m, copy_I, CategoryTheory.Limits.ImageFactorisation.copy_F, copy_e, CategoryTheory.Limits.IsImage.copy_lift
e 📖	CompOp	31 math math: fac, CategoryTheory.Limits.IsImage.e_isoExt_inv, ofArrowIso_e, CategoryTheory.Limits.as_factorThruImage, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_e, CategoryTheory.Limits.monoFactorisationZero_e, CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation, CategoryTheory.Limits.image.fac_lift, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e, isoComp_e, fac_assoc, CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi, CategoryTheory.Limits.image.fac_lift_assoc, compMono_e, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison, ofIsoComp_e, CategoryTheory.Limits.IsImage.e_isoExt_hom, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', CategoryTheory.Limits.IsImage.self_lift, CategoryTheory.Regular.frobeniusMorphism_isPullback, kernel_ι_comp, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, ofIsoI_e, CategoryTheory.Limits.IsImage.fac_lift, fac_apply, CategoryTheory.Regular.instIsRegularEpiEStrongEpiMonoFactorisation, CategoryTheory.Limits.IsImage.fac_lift_assoc, CategoryTheory.FunctorToTypes.monoFactorisation_e, ofCompIso_e
instInhabitedOfMono 📖	CompOp	—
isoComp 📖	CompOp	3 math math: isoComp_e, isoComp_I, isoComp_m
m 📖	CompOp	31 math math: fac, AddCommGrpCat.image.lift_fac, CategoryTheory.Subobject.imageFactorisation_F_m, CategoryTheory.Limits.IsImage.lift_ι_assoc, compMono_m, CategoryTheory.Limits.IsImage.lift_fac, m_mono, CategoryTheory.Limits.image.lift_fac_assoc, fac_assoc, CategoryTheory.Limits.monoFactorisationZero_m, ModuleCat.image.lift_fac, CategoryTheory.Limits.IsImage.isoExt_inv_m, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m, CategoryTheory.Limits.image.lift_fac, CategoryTheory.Limits.IsImage.isoExt_hom_m, ofCompIso_m, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m, ofArrowIso_m, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi, ofIsoI_m, CategoryTheory.Limits.IsImage.lift_fac_assoc, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.Limits.IsImage.lift_ι, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, CategoryTheory.Limits.image.as_ι, CategoryTheory.FunctorToTypes.monoFactorisation_m, fac_apply, CategoryTheory.Limits.Types.Image.lift_fac, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_m, isoComp_m, ofIsoComp_m
ofArrowIso 📖	CompOp	5 math math: ofArrowIso_e, CategoryTheory.Limits.IsImage.ofArrowIso_lift, CategoryTheory.Limits.ImageFactorisation.ofArrowIso_F, ofArrowIso_m, ofArrowIso_I
ofCompIso 📖	CompOp	3 math math: ofCompIso_m, ofCompIso_I, ofCompIso_e
ofIsoComp 📖	CompOp	3 math math: ofIsoComp_e, ofIsoComp_I, ofIsoComp_m
ofIsoI 📖	CompOp	5 math math: CategoryTheory.Limits.IsImage.ofIsoI_lift, CategoryTheory.Limits.ImageFactorisation.ofIsoI_F, ofIsoI_I, ofIsoI_m, ofIsoI_e
self 📖	CompOp	1 math math: CategoryTheory.Limits.IsImage.self_lift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMono_I 📖	mathematical	—	I CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct compMono	—	—
compMono_e 📖	mathematical	—	e CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct compMono	—	—
compMono_m 📖	mathematical	—	m CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct compMono I	—	—
copy_I 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct I m e	copy	—	—
copy_e 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct I m e	copy	—	—
copy_m 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct I m e	copy	—	—
ext 📖	—	I m CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—	CategoryTheory.Category.id_comp CategoryTheory.cancel_mono
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I e m	—	—
fac_apply 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types I CategoryTheory.Functor CategoryTheory.Functor.category m e	—	fac
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I e m	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
isoComp_I 📖	mathematical	—	I CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct isoComp	—	—
isoComp_e 📖	mathematical	—	e CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct isoComp I	—	—
isoComp_m 📖	mathematical	—	m CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct isoComp	—	—
m_mono 📖	mathematical	—	CategoryTheory.Mono I m	—	—
ofArrowIso_I 📖	mathematical	—	I CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom ofArrowIso	—	—
ofArrowIso_e 📖	mathematical	—	e CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom ofArrowIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.inv CategoryTheory.CommaMorphism.left CategoryTheory.Arrow.isIso_left	—	—
ofArrowIso_m 📖	mathematical	—	m CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom ofArrowIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.CommaMorphism.right	—	—
ofCompIso_I 📖	mathematical	—	I ofCompIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ofCompIso_e 📖	mathematical	—	e ofCompIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ofCompIso_m 📖	mathematical	—	m ofCompIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.inv	—	—
ofIsoComp_I 📖	mathematical	—	I ofIsoComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ofIsoComp_e 📖	mathematical	—	e ofIsoComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.inv	—	—
ofIsoComp_m 📖	mathematical	—	m ofIsoComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ofIsoI_I 📖	mathematical	—	I ofIsoI	—	—
ofIsoI_e 📖	mathematical	—	e ofIsoI CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.Iso.hom	—	—
ofIsoI_m 📖	mathematical	—	m ofIsoI CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.Iso.inv	—	—

CategoryTheory.Limits.StrongEpiMonoFactorisation

Definitions

Name	Category	Theorems
toMonoFactorisation 📖	CompOp	12 math math: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_e, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e, e_strong_epi, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_I, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_I, CategoryTheory.Regular.instIsRegularEpiEStrongEpiMonoFactorisation, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_m
toMonoIsImage 📖	CompOp	1 math math: CategoryTheory.PreservesImage.iso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
e_strong_epi 📖	mathematical	—	CategoryTheory.StrongEpi CategoryTheory.Limits.MonoFactorisation.I toMonoFactorisation CategoryTheory.Limits.MonoFactorisation.e	—	—

CategoryTheory.Limits.image

Definitions

Name	Category	Theorems
compIso 📖	CompOp	4 math math: compIso_hom_comp_image_ι, compIso_hom_comp_image_ι_assoc, compIso_inv_comp_image_ι_assoc, compIso_inv_comp_image_ι
eqToHom 📖	CompOp	2 math math: CategoryTheory.Limits.instIsIsoEqToHom, preComp_comp
eqToIso 📖	CompOp	1 math math: eq_fac
isoStrongEpiMono 📖	CompOp	2 math math: isoStrongEpiMono_hom_comp_ι, isoStrongEpiMono_inv_comp_mono
map 📖	CompOp	8 math math: map_id, map_comp, map_ι, map_homMk'_ι, CategoryTheory.Limits.imageSubobjectIso_comp_image_map, CategoryTheory.Limits.im_map, CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv, factor_map
preComp 📖	CompOp	8 math math: isIso_precomp_iso, preComp_epi_of_epi, factorThruImage_preComp, preComp_ι, factorThruImage_preComp_assoc, preComp_mono, preComp_comp, preComp_ι_assoc
ι 📖	CompOp	68 math math: CategoryTheory.Limits.imageSubobject_arrow_assoc, CategoryTheory.Limits.cokernelImageι_inv, CategoryTheory.Limits.IsImage.lift_ι_assoc, SimplexCategory.image_ι_eq, SimplicialObject.Splitting.IndexSet.fac_pull_assoc, compIso_hom_comp_image_ι, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', compIso_hom_comp_image_ι_assoc, lift_mk_factorThruImage, eq_fac, lift_fac_assoc, isoStrongEpiMono_hom_comp_ι, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι, CategoryTheory.image_ι_op_comp_imageUnopOp_hom, map_ι, ModuleCat.imageIsoRange_hom_subtype, ModuleCat.imageIsoRange_inv_image_ι_apply, CategoryTheory.Limits.imageMonoIsoSource_hom_self, CategoryTheory.PreservesImage.iso_hom, CategoryTheory.MonoOver.image_map, ι_zero, map_homMk'_ι, CategoryTheory.PreservesImage.hom_comp_map_image_ι, CategoryTheory.factorThruImage_comp_imageUnopOp_inv, isoStrongEpiMono_inv_comp_mono, CategoryTheory.PreservesImage.inv_comp_image_ι_map, CategoryTheory.Abelian.imageIsoImage_inv, lift_fac, CategoryTheory.Limits.imageMonoIsoSource_inv_ι, fac, ModuleCat.imageIsoRange_hom_subtype_assoc, preComp_ι, SimplicialObject.Splitting.IndexSet.fac_pull, ModuleCat.imageIsoRange_inv_image_ι, CategoryTheory.MonoOver.imageMonoOver_arrow, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, CategoryTheory.Limits.instMonoι, ModuleCat.imageIsoRange_inv_image_ι_assoc, CategoryTheory.Limits.imageSubobject_arrow, CategoryTheory.Limits.ImageMap.map_ι, CategoryTheory.Limits.imageSubobject_arrow'_assoc, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι, CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι, CategoryTheory.imageUnopOp_hom_comp_image_ι, CategoryTheory.Limits.image_ι_comp_eq_zero, fac_assoc, CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc, CategoryTheory.Limits.IsImage.lift_ι, ι_zero', as_ι, CategoryTheory.Limits.epi_image_of_epi, CategoryTheory.Limits.imageMonoIsoSource_inv_ι_assoc, lift_mk_factorThruImage_assoc, CategoryTheory.Limits.ImageMap.map_ι_assoc, compIso_inv_comp_image_ι_assoc, preComp_ι_assoc, CategoryTheory.PreservesImage.iso_inv, CategoryTheory.Limits.imageMonoIsoSource_hom_self_assoc, CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', ModuleCat.imageIsoRange_hom_subtype_apply, CategoryTheory.Limits.imageSubobject_arrow', CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc, CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc, CategoryTheory.Limits.cokernelImageι_hom, compIso_inv_comp_image_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
as_ι 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Limits.Image.monoFactorisation ι	—	—
compIso_hom_comp_image_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Iso.hom compIso ι	—	ext CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Limits.hasLimitOfHasLimitsOfShape fac_lift_assoc fac fac_assoc
compIso_hom_comp_image_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Iso.hom compIso ι	—	CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' compIso_hom_comp_image_ι
compIso_inv_comp_image_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Iso.inv compIso ι CategoryTheory.inv	—	ext CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Limits.hasLimitOfHasLimitsOfShape fac_lift_assoc fac fac_assoc CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
compIso_inv_comp_image_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Iso.inv compIso ι CategoryTheory.inv	—	CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' compIso_inv_comp_image_ι
eq_fac 📖	mathematical	—	ι CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Iso.hom eqToIso	—	ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape fac lift_mk_factorThruImage
ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.factorThruImage	—	—	CategoryTheory.mono_comp CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Limits.instMonoι CategoryTheory.Limits.limit.lift_π_assoc fac lift_fac CategoryTheory.cancel_mono_id CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.equalizer.condition
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.factorThruImage ι	—	CategoryTheory.Limits.MonoFactorisation.fac
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.factorThruImage ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
fac_lift 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.factorThruImage lift CategoryTheory.Limits.MonoFactorisation.e	—	CategoryTheory.Limits.IsImage.fac_lift
fac_lift_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.factorThruImage CategoryTheory.Limits.MonoFactorisation.I lift CategoryTheory.Limits.MonoFactorisation.e	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac_lift
factorThruImage_preComp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.factorThruImage preComp	—	fac_lift CategoryTheory.Limits.instMonoι
factorThruImage_preComp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.factorThruImage preComp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThruImage_preComp
factor_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Limits.image CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.factorThruImage map CategoryTheory.CommaMorphism.left	—	CategoryTheory.Limits.ImageMap.factor_map
isImage_lift 📖	mathematical	—	CategoryTheory.Limits.IsImage.lift CategoryTheory.Limits.Image.monoFactorisation CategoryTheory.Limits.Image.isImage lift	—	—
isIso_precomp_iso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.image CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.hasImage_iso_comp preComp	—	CategoryTheory.Limits.hasImage_iso_comp CategoryTheory.Limits.instMonoι CategoryTheory.Category.assoc fac CategoryTheory.IsIso.inv_hom_id_assoc ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape fac_lift_assoc fac_lift CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Category.comp_id
isoStrongEpiMono_hom_comp_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Iso.hom isoStrongEpiMono ι	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Limits.IsImage.lift_fac
isoStrongEpiMono_inv_comp_mono 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Iso.inv isoStrongEpiMono ι	—	lift_fac
lift_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.MonoFactorisation.I lift CategoryTheory.Limits.MonoFactorisation.m ι	—	CategoryTheory.Limits.IsImage.lift_fac
lift_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.MonoFactorisation.I lift CategoryTheory.Limits.MonoFactorisation.m ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fac
lift_mk_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image ι	CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.instMonoι lift	—	lift_fac CategoryTheory.Limits.instMonoι
lift_mk_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image ι	lift CategoryTheory.Limits.instMonoι	—	CategoryTheory.Limits.instMonoι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_mk_comp
lift_mk_factorThruImage 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.MonoFactorisation.I ι CategoryTheory.Limits.instMonoι CategoryTheory.Limits.factorThruImage lift	—	CategoryTheory.Limits.IsImage.lift_fac CategoryTheory.Limits.instMonoι
lift_mk_factorThruImage_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image lift ι CategoryTheory.Limits.instMonoι CategoryTheory.Limits.factorThruImage	—	CategoryTheory.Limits.instMonoι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_mk_factorThruImage
lift_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.image CategoryTheory.Limits.MonoFactorisation.I lift	—	CategoryTheory.mono_of_mono lift_fac CategoryTheory.Limits.MonoFactorisation.m_mono
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.instSubsingletonImageMap
map_homMk'_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.instHasImageHomMk map CategoryTheory.Arrow.homMk' ι	—	CategoryTheory.Limits.instHasImageHomMk map_ι
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.instSubsingletonImageMap
map_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom map ι CategoryTheory.CommaMorphism.right	—	CategoryTheory.Limits.ImageMap.map_ι
preComp_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image preComp eqToHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.assoc	—	CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.Limits.instMonoι lift_mk_comp fac lift_fac
preComp_epi_of_epi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.image CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct preComp	—	CategoryTheory.epi_of_epi_fac CategoryTheory.epi_comp CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair CategoryTheory.Limits.hasLimitOfHasLimitsOfShape factorThruImage_preComp
preComp_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.image CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct preComp	—	CategoryTheory.mono_of_mono preComp_ι CategoryTheory.Limits.instMonoι
preComp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image preComp ι	—	lift_mk_comp CategoryTheory.Category.assoc fac
preComp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image preComp ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' preComp_ι

---

← Back to Index