Limits

📁 Source: Mathlib/CategoryTheory/Subobject/Limits.lean

Statistics

Metric	Count
Definitions cokernelOrderHom, equalizerSubobject, equalizerSubobjectIso, factorThruImageSubobject, factorThruKernelSubobject, imageSubobject, imageSubobjectCompIso, imageSubobjectIso, imageSubobjectMap, kernelOrderHom, kernelSubobject, kernelSubobjectIso, kernelSubobjectIsoComp, kernelSubobjectMap	14
Theorems cokernelOrderHom_coe, equalizerSubobject_arrow, equalizerSubobject_arrow', equalizerSubobject_arrow'_assoc, equalizerSubobject_arrow_assoc, equalizerSubobject_arrow_comp, equalizerSubobject_arrow_comp_assoc, equalizerSubobject_factors, equalizerSubobject_factors_iff, equalizerSubobject_of_self, factorThruImageSubobject_comp_self, factorThruImageSubobject_comp_self_assoc, factorThruKernelSubobject_comp_arrow, factorThruKernelSubobject_comp_kernelSubobjectIso, imageSubobjectCompIso_hom_arrow, imageSubobjectCompIso_hom_arrow_assoc, imageSubobjectCompIso_inv_arrow, imageSubobjectCompIso_inv_arrow_assoc, imageSubobjectIso_comp_image_map, imageSubobjectMap_arrow, imageSubobjectMap_arrow_assoc, imageSubobject_arrow, imageSubobject_arrow', imageSubobject_arrow'_assoc, imageSubobject_arrow_assoc, imageSubobject_arrow_comp, imageSubobject_arrow_comp_apply, imageSubobject_arrow_comp_assoc, imageSubobject_arrow_comp_eq_zero, imageSubobject_comp_le, imageSubobject_comp_le_epi_of_epi, imageSubobject_factors_comp_self, imageSubobject_iso_comp, imageSubobject_le, imageSubobject_le_mk, imageSubobject_mono, imageSubobject_zero, imageSubobject_zero_arrow, image_map_comp_imageSubobjectIso_inv, instEpiFactorThruImageSubobjectOfHasEqualizers, isIso_kernelSubobject_zero_arrow, kernelOrderHom_coe, kernelSubobjectIsoComp_hom_arrow, kernelSubobjectIsoComp_inv_arrow, kernelSubobjectIso_comp_kernel_map, kernelSubobjectIso_comp_kernel_map_assoc, kernelSubobjectMap_arrow, kernelSubobjectMap_arrow_apply, kernelSubobjectMap_arrow_assoc, kernelSubobjectMap_comp, kernelSubobjectMap_id, kernelSubobject_arrow, kernelSubobject_arrow', kernelSubobject_arrow'_apply, kernelSubobject_arrow'_assoc, kernelSubobject_arrow_apply, kernelSubobject_arrow_assoc, kernelSubobject_arrow_comp, kernelSubobject_arrow_comp_apply, kernelSubobject_arrow_comp_assoc, kernelSubobject_comp_le, kernelSubobject_comp_mono, kernelSubobject_comp_mono_isIso, kernelSubobject_factors, kernelSubobject_factors_iff, kernelSubobject_zero, kernel_map_comp_kernelSubobjectIso_inv, kernel_map_comp_kernelSubobjectIso_inv_assoc, le_kernelSubobject, pullback_equalizer, pullback_factors, pullback_factors_iff	72
Total	86

CategoryTheory.Limits

Definitions

Name	Category	Theorems
cokernelOrderHom 📖	CompOp	1 math math: cokernelOrderHom_coe
equalizerSubobject 📖	CompOp	10 math math: equalizerSubobject_arrow'_assoc, equalizerSubobject_arrow_comp, equalizerSubobject_factors_iff, equalizerSubobject_arrow, equalizerSubobject_of_self, equalizerSubobject_arrow', equalizerSubobject_arrow_comp_assoc, equalizerSubobject_arrow_assoc, equalizerSubobject_factors, pullback_equalizer
equalizerSubobjectIso 📖	CompOp	4 math math: equalizerSubobject_arrow'_assoc, equalizerSubobject_arrow, equalizerSubobject_arrow', equalizerSubobject_arrow_assoc
factorThruImageSubobject 📖	CompOp	7 math math: factorThruImageSubobject_comp_imageToKernel, factorThruImageSubobject_comp_self_assoc, imageSubobject_arrow_comp_apply, imageSubobject_arrow_comp_assoc, imageSubobject_arrow_comp, instEpiFactorThruImageSubobjectOfHasEqualizers, factorThruImageSubobject_comp_self
factorThruKernelSubobject 📖	CompOp	3 math math: factorThruImageSubobject_comp_imageToKernel, factorThruKernelSubobject_comp_arrow, factorThruKernelSubobject_comp_kernelSubobjectIso
imageSubobject 📖	CompOp	52 math math: imageSubobject_arrow_assoc, imageSubobjectCompIso_hom_arrow, imageToKernel_unop, imageToKernel'_kernelSubobjectIso, imageSubobject_arrow_comp_eq_zero, imageToKernel_op, factorThruImageSubobject_comp_imageToKernel, imageToKernel_comp_right, imageToKernel_comp_hom_inv_comp, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel, imageToKernel_arrow_assoc, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, imageToKernel_epi_comp, imageSubobjectIso_comp_image_map, imageSubobject_zero_arrow, subobject_ofLE_as_imageToKernel, imageSubobject_zero, imageSubobject_le_mk, imageToKernel_arrow, image_le_kernel, imageSubobject_arrow_comp_apply, imageToKernel_epi_of_zero_of_mono, imageToKernel_comp_left, imageSubobjectCompIso_inv_arrow_assoc, imageSubobjectMap_arrow, imageSubobjectMap_arrow_assoc, imageSubobject_comp_le, imageSubobjectIso_imageToKernel', imageSubobject_arrow, imageSubobject_comp_le_epi_of_epi, instMonoImageToKernel, imageSubobject_arrow_comp_assoc, imageSubobject_iso_comp, imageSubobject_arrow'_assoc, HomologicalComplex.image_eq_image, imageSubobject_le, imageSubobjectCompIso_hom_arrow_assoc, imageToKernel_arrow_apply, HomologicalComplex.image_to_eq_image, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel, CategoryTheory.ShortComplex.exact_iff_image_eq_kernel, imageToKernel_zero_right, imageSubobjectCompIso_inv_arrow, image_map_comp_imageSubobjectIso_inv, imageSubobject_arrow_comp, imageSubobject_mono, imageToKernel_zero_left, imageToKernel_epi_of_epi_of_zero, imageSubobject_arrow', imageToKernel_comp_mono, instEpiFactorThruImageSubobjectOfHasEqualizers, imageSubobject_factors_comp_self
imageSubobjectCompIso 📖	CompOp	5 math math: imageSubobjectCompIso_hom_arrow, imageToKernel_comp_hom_inv_comp, imageSubobjectCompIso_inv_arrow_assoc, imageSubobjectCompIso_hom_arrow_assoc, imageSubobjectCompIso_inv_arrow
imageSubobjectIso 📖	CompOp	10 math math: imageSubobject_arrow_assoc, imageToKernel_unop, imageToKernel'_kernelSubobjectIso, imageToKernel_op, imageSubobjectIso_comp_image_map, imageSubobjectIso_imageToKernel', imageSubobject_arrow, imageSubobject_arrow'_assoc, image_map_comp_imageSubobjectIso_inv, imageSubobject_arrow'
imageSubobjectMap 📖	CompOp	4 math math: imageSubobjectIso_comp_image_map, imageSubobjectMap_arrow, imageSubobjectMap_arrow_assoc, image_map_comp_imageSubobjectIso_inv
kernelOrderHom 📖	CompOp	1 math math: kernelOrderHom_coe
kernelSubobject 📖	CompOp	59 math math: kernelSubobjectMap_arrow_assoc, AlgebraicTopology.NormalizedMooreComplex.obj_d, imageToKernel_unop, imageToKernel'_kernelSubobjectIso, kernelSubobject_arrow'_apply, kernelSubobjectIsoComp_hom_arrow, imageToKernel_op, factorThruImageSubobject_comp_imageToKernel, kernelSubobject_arrow_assoc, kernelSubobjectMap_comp, kernelSubobject_comp_mono_isIso, imageToKernel_comp_right, imageToKernel_comp_hom_inv_comp, factorThruKernelSubobject_comp_arrow, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel, kernelSubobject_factors, imageToKernel_arrow_assoc, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, imageToKernel_epi_comp, kernelSubobjectIso_comp_kernel_map, subobject_ofLE_as_imageToKernel, kernelSubobjectIsoComp_inv_arrow, imageToKernel_arrow, image_le_kernel, kernelSubobject_arrow_comp_apply, imageToKernel_epi_of_zero_of_mono, kernelSubobjectIso_comp_kernel_map_assoc, imageToKernel_comp_left, kernelSubobject_arrow, kernelSubobject_factors_iff, imageSubobjectIso_imageToKernel', instMonoImageToKernel, isIso_kernelSubobject_zero_arrow, HomologicalComplex.kernel_from_eq_kernel, kernel_map_comp_kernelSubobjectIso_inv, imageToKernel_arrow_apply, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel, CategoryTheory.ShortComplex.exact_iff_image_eq_kernel, kernelSubobject_comp_mono, kernelSubobject_arrow'_assoc, imageToKernel_zero_right, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, le_kernelSubobject, kernelSubobject_arrow_comp_assoc, kernel_map_comp_kernelSubobjectIso_inv_assoc, kernelSubobject_arrow_apply, imageToKernel_zero_left, imageToKernel_epi_of_epi_of_zero, kernelSubobject_arrow_comp, factorThruKernelSubobject_comp_kernelSubobjectIso, kernelSubobjectMap_arrow, ModuleCat.toKernelSubobject_arrow, imageToKernel_comp_mono, kernelSubobject_arrow', HomologicalComplex.kernel_eq_kernel, kernelSubobject_comp_le, kernelSubobjectMap_arrow_apply, kernelSubobjectMap_id, kernelSubobject_zero
kernelSubobjectIso 📖	CompOp	15 math math: imageToKernel_unop, imageToKernel'_kernelSubobjectIso, kernelSubobject_arrow'_apply, imageToKernel_op, kernelSubobject_arrow_assoc, kernelSubobjectIso_comp_kernel_map, kernelSubobjectIso_comp_kernel_map_assoc, kernelSubobject_arrow, imageSubobjectIso_imageToKernel', kernel_map_comp_kernelSubobjectIso_inv, kernelSubobject_arrow'_assoc, kernel_map_comp_kernelSubobjectIso_inv_assoc, kernelSubobject_arrow_apply, factorThruKernelSubobject_comp_kernelSubobjectIso, kernelSubobject_arrow'
kernelSubobjectIsoComp 📖	CompOp	3 math math: kernelSubobjectIsoComp_hom_arrow, imageToKernel_comp_hom_inv_comp, kernelSubobjectIsoComp_inv_arrow
kernelSubobjectMap 📖	CompOp	9 math math: kernelSubobjectMap_arrow_assoc, kernelSubobjectMap_comp, kernelSubobjectIso_comp_kernel_map, kernelSubobjectIso_comp_kernel_map_assoc, kernel_map_comp_kernelSubobjectIso_inv, kernel_map_comp_kernelSubobjectIso_inv_assoc, kernelSubobjectMap_arrow, kernelSubobjectMap_arrow_apply, kernelSubobjectMap_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokernelOrderHom_coe 📖	mathematical	—	DFunLike.coe OrderHom CategoryTheory.Subobject OrderDual Opposite CategoryTheory.Category.opposite Opposite.op PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject OrderDual.instPreorder OrderHom.instFunLike cokernelOrderHom CategoryTheory.Subobject.lift cokernel HasCokernels.has_colimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct cokernel.π	—	—
equalizerSubobject_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying equalizerSubobject equalizer CategoryTheory.Iso.hom equalizerSubobjectIso equalizer.ι CategoryTheory.Subobject.arrow	—	equalizer.ι_mono
equalizerSubobject_arrow' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct equalizer CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying equalizerSubobject CategoryTheory.Iso.inv equalizerSubobjectIso CategoryTheory.Subobject.arrow equalizer.ι	—	CategoryTheory.Subobject.underlyingIso_arrow equalizer.ι_mono
equalizerSubobject_arrow'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct equalizer CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying equalizerSubobject CategoryTheory.Iso.inv equalizerSubobjectIso CategoryTheory.Subobject.arrow equalizer.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerSubobject_arrow'
equalizerSubobject_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying equalizerSubobject equalizer CategoryTheory.Iso.hom equalizerSubobjectIso equalizer.ι CategoryTheory.Subobject.arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerSubobject_arrow
equalizerSubobject_arrow_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying equalizerSubobject CategoryTheory.Subobject.arrow	—	equalizerSubobject_arrow CategoryTheory.Category.assoc equalizer.condition
equalizerSubobject_arrow_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying equalizerSubobject CategoryTheory.Subobject.arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerSubobject_arrow_comp
equalizerSubobject_factors 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Subobject.Factors equalizerSubobject	—	equalizer.ι_mono limit.lift_π
equalizerSubobject_factors_iff 📖	mathematical	—	CategoryTheory.Subobject.Factors equalizerSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Subobject.factorThru_arrow CategoryTheory.Category.assoc equalizerSubobject_arrow_comp equalizerSubobject_factors
equalizerSubobject_of_self 📖	mathematical	—	equalizerSubobject hasEqualizer_of_self Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.orderTop	—	CategoryTheory.Subobject.mk_eq_top_of_isIso hasEqualizer_of_self equalizer.ι_of_self
factorThruImageSubobject_comp_self 📖	mathematical	CategoryTheory.Subobject.Factors imageSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Subobject.factorThru CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying factorThruImageSubobject	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Subobject.factorThru_arrow CategoryTheory.Category.assoc imageSubobject_arrow_comp
factorThruImageSubobject_comp_self_assoc 📖	mathematical	CategoryTheory.Subobject.Factors imageSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Subobject.factorThru CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying factorThruImageSubobject	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Subobject.factorThru_arrow CategoryTheory.Category.assoc imageSubobject_arrow_comp
factorThruKernelSubobject_comp_arrow 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject factorThruKernelSubobject CategoryTheory.Subobject.arrow	—	kernelSubobject_factors CategoryTheory.Subobject.factorThru_arrow
factorThruKernelSubobject_comp_kernelSubobjectIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernel factorThruKernelSubobject CategoryTheory.Iso.hom kernelSubobjectIso kernel.lift	—	CategoryTheory.cancel_mono equalizer.ι_mono CategoryTheory.Category.assoc kernelSubobject_arrow factorThruKernelSubobject_comp_arrow kernel.lift_ι
imageSubobjectCompIso_hom_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject hasImage_comp_iso CategoryTheory.Iso.hom imageSubobjectCompIso CategoryTheory.Subobject.arrow CategoryTheory.inv	—	hasImage_comp_iso CategoryTheory.Category.assoc imageSubobject_arrow' image.compIso_inv_comp_image_ι imageSubobject_arrow_assoc
imageSubobjectCompIso_hom_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject hasImage_comp_iso CategoryTheory.Iso.hom imageSubobjectCompIso CategoryTheory.Subobject.arrow CategoryTheory.inv	—	hasImage_comp_iso CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageSubobjectCompIso_hom_arrow
imageSubobjectCompIso_inv_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject hasImage_comp_iso CategoryTheory.Iso.inv imageSubobjectCompIso CategoryTheory.Subobject.arrow	—	hasImage_comp_iso CategoryTheory.Category.assoc imageSubobject_arrow' image.compIso_hom_comp_image_ι imageSubobject_arrow_assoc
imageSubobjectCompIso_inv_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject hasImage_comp_iso CategoryTheory.Iso.inv imageSubobjectCompIso CategoryTheory.Subobject.arrow	—	hasImage_comp_iso CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageSubobjectCompIso_inv_arrow
imageSubobjectIso_comp_image_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Functor.id CategoryTheory.Comma.right Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject CategoryTheory.Comma.left CategoryTheory.Comma.hom instHasImageHomMk image CategoryTheory.Iso.hom imageSubobjectIso image.map imageSubobjectMap	—	instHasImageHomMk CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
imageSubobjectMap_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject imageSubobjectMap CategoryTheory.Subobject.arrow CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	instHasImageHomMk CategoryTheory.Category.assoc imageSubobject_arrow' image.map_ι imageSubobject_arrow
imageSubobjectMap_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject imageSubobjectMap CategoryTheory.Subobject.arrow CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id	—	instHasImageHomMk CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageSubobjectMap_arrow
imageSubobject_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject image CategoryTheory.Iso.hom imageSubobjectIso image.ι CategoryTheory.Subobject.arrow	—	instMonoι
imageSubobject_arrow' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject CategoryTheory.Iso.inv imageSubobjectIso CategoryTheory.Subobject.arrow image.ι	—	CategoryTheory.Subobject.underlyingIso_arrow instMonoι
imageSubobject_arrow'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject CategoryTheory.Iso.inv imageSubobjectIso CategoryTheory.Subobject.arrow image.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageSubobject_arrow'
imageSubobject_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject image CategoryTheory.Iso.hom imageSubobjectIso image.ι CategoryTheory.Subobject.arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageSubobject_arrow
imageSubobject_arrow_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject factorThruImageSubobject CategoryTheory.Subobject.arrow	—	CategoryTheory.Category.assoc imageSubobject_arrow' image.fac
imageSubobject_arrow_comp_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject CategoryTheory.ConcreteCategory.hom CategoryTheory.Subobject.arrow factorThruImageSubobject	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise imageSubobject_arrow_comp
imageSubobject_arrow_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject factorThruImageSubobject CategoryTheory.Subobject.arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageSubobject_arrow_comp
imageSubobject_arrow_comp_eq_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject CategoryTheory.Subobject.arrow	—	zero_of_epi_comp imageSubobject_arrow_comp_assoc
imageSubobject_comp_le 📖	mathematical	—	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject imageSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Subobject.mk_le_mk_of_comm instMonoι image.preComp_ι
imageSubobject_comp_le_epi_of_epi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Subobject.ofLE imageSubobject_comp_le	—	imageSubobject_comp_le instMonoι CategoryTheory.Subobject.mk_le_mk_of_comm image.preComp_ι CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm CategoryTheory.epi_comp CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom image.preComp_epi_of_epi CategoryTheory.Iso.isIso_inv
imageSubobject_factors_comp_self 📖	mathematical	—	CategoryTheory.Subobject.Factors imageSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	instMonoι CategoryTheory.Category.assoc image.fac
imageSubobject_iso_comp 📖	mathematical	—	imageSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasImage_iso_comp	—	le_antisymm hasImage_iso_comp imageSubobject_comp_le CategoryTheory.Subobject.mk_le_mk_of_comm instMonoι image.isIso_precomp_iso image.preComp_ι
imageSubobject_le 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Subobject.arrow	Preorder.toLE imageSubobject	—	CategoryTheory.Subobject.le_of_comm CategoryTheory.Subobject.arrow_mono CategoryTheory.Category.assoc image.lift_fac imageSubobject_arrow
imageSubobject_le_mk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject imageSubobject	—	imageSubobject_le CategoryTheory.Category.assoc CategoryTheory.Subobject.underlyingIso_arrow
imageSubobject_mono 📖	mathematical	—	imageSubobject mono_hasImage	—	CategoryTheory.Subobject.eq_of_comm mono_hasImage CategoryTheory.Category.assoc CategoryTheory.Subobject.underlyingIso_arrow imageMonoIsoSource_hom_self imageSubobject_arrow
imageSubobject_zero 📖	mathematical	—	imageSubobject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasImage_zero Bot.bot CategoryTheory.Subobject OrderBot.toBot Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.orderBot HasZeroObject.hasInitial HasZeroObject.initialMonoClass	—	CategoryTheory.Subobject.eq_of_comm hasImage_zero HasZeroObject.hasInitial HasZeroObject.initialMonoClass CategoryTheory.Subobject.bot_arrow comp_zero imageSubobject_zero_arrow
imageSubobject_zero_arrow 📖	mathematical	—	CategoryTheory.Subobject.arrow imageSubobject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasImage_zero CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying	—	hasImage_zero imageSubobject_arrow image.ι_zero comp_zero
image_map_comp_imageSubobjectIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom instHasImageHomMk CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject image.map CategoryTheory.Iso.inv imageSubobjectIso imageSubobjectMap	—	instHasImageHomMk CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Category.assoc imageSubobject_arrow' imageSubobjectMap_arrow imageSubobject_arrow'_assoc image.map_ι
instEpiFactorThruImageSubobjectOfHasEqualizers 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying imageSubobject factorThruImageSubobject	—	CategoryTheory.epi_comp instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair hasLimitOfHasLimitsOfShape CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv
isIso_kernelSubobject_zero_arrow 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasEqualizer_of_self CategoryTheory.Subobject.arrow	—	hasEqualizer_of_self CategoryTheory.Subobject.isIso_arrow_iff_eq_top equalizerSubobject_of_self
kernelOrderHom_coe 📖	mathematical	—	DFunLike.coe OrderHom OrderDual CategoryTheory.Subobject Opposite CategoryTheory.Category.opposite Opposite.op OrderDual.instPreorder PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject OrderHom.instFunLike kernelOrderHom CategoryTheory.Subobject.lift kernel Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct kernel.ι	—	—
kernelSubobjectIsoComp_hom_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject hasKernel_iso_comp CategoryTheory.Iso.hom kernelSubobjectIsoComp CategoryTheory.Subobject.arrow	—	hasKernel_iso_comp CategoryTheory.Category.assoc kernelSubobject_arrow' kernel.lift_ι kernelSubobject_arrow_assoc
kernelSubobjectIsoComp_inv_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject hasKernel_iso_comp CategoryTheory.Iso.inv kernelSubobjectIsoComp CategoryTheory.Subobject.arrow CategoryTheory.inv	—	hasKernel_iso_comp CategoryTheory.Category.assoc kernelSubobject_arrow' kernel.lift_ι kernelSubobject_arrow_assoc
kernelSubobjectIso_comp_kernel_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernel CategoryTheory.Iso.hom kernelSubobjectIso kernel.map CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.w kernelSubobjectMap	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.assoc kernel_map_comp_kernelSubobjectIso_inv CategoryTheory.Iso.hom_inv_id_assoc
kernelSubobjectIso_comp_kernel_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernel CategoryTheory.Iso.hom kernelSubobjectIso kernel.map CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.w kernelSubobjectMap	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelSubobjectIso_comp_kernel_map
kernelSubobjectMap_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernelSubobjectMap CategoryTheory.Subobject.arrow CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left	—	CategoryTheory.Subobject.factorThru_arrow
kernelSubobjectMap_arrow_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.ConcreteCategory.hom CategoryTheory.Subobject.arrow kernelSubobjectMap CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise kernelSubobjectMap_arrow
kernelSubobjectMap_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernelSubobjectMap CategoryTheory.Subobject.arrow CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelSubobjectMap_arrow
kernelSubobjectMap_comp 📖	mathematical	—	kernelSubobjectMap CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq kernelSubobjectMap_arrow CategoryTheory.Category.assoc kernelSubobjectMap_arrow_assoc
kernelSubobjectMap_id 📖	mathematical	—	kernelSubobjectMap CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq kernelSubobjectMap_arrow CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
kernelSubobject_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernel CategoryTheory.Iso.hom kernelSubobjectIso kernel.ι CategoryTheory.Subobject.arrow	—	—
kernelSubobject_arrow' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.Iso.inv kernelSubobjectIso CategoryTheory.Subobject.arrow kernel.ι	—	CategoryTheory.Subobject.underlyingIso_arrow
kernelSubobject_arrow'_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.ConcreteCategory.hom CategoryTheory.Subobject.arrow kernel CategoryTheory.Iso.inv kernelSubobjectIso kernel.ι	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise kernelSubobject_arrow'
kernelSubobject_arrow'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.Iso.inv kernelSubobjectIso CategoryTheory.Subobject.arrow kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelSubobject_arrow'
kernelSubobject_arrow_apply 📖	mathematical	—	DFunLike.coe kernel CategoryTheory.ConcreteCategory.hom kernel.ι CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.Iso.hom kernelSubobjectIso CategoryTheory.Subobject.arrow	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise kernelSubobject_arrow
kernelSubobject_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernel CategoryTheory.Iso.hom kernelSubobjectIso kernel.ι CategoryTheory.Subobject.arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelSubobject_arrow
kernelSubobject_arrow_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.Subobject.arrow Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	—	kernelSubobject_arrow CategoryTheory.Category.assoc kernel.condition comp_zero
kernelSubobject_arrow_comp_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.Subobject.arrow Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise kernelSubobject_arrow_comp
kernelSubobject_arrow_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.Subobject.arrow Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelSubobject_arrow_comp
kernelSubobject_comp_le 📖	mathematical	—	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject kernelSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	le_kernelSubobject kernelSubobject_arrow_comp_assoc zero_comp
kernelSubobject_comp_mono 📖	mathematical	—	kernelSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasKernel_comp_mono	—	le_antisymm hasKernel_comp_mono le_kernelSubobject CategoryTheory.cancel_mono CategoryTheory.Category.assoc kernelSubobject_arrow_comp zero_comp kernelSubobject_comp_le
kernelSubobject_comp_mono_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasKernel_comp_mono CategoryTheory.Subobject.ofLE kernelSubobject_comp_le	—	hasKernel_comp_mono kernelSubobject_comp_le CategoryTheory.Subobject.mk_le_mk_of_comm kernel.lift_ι CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv
kernelSubobject_factors 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Subobject.Factors kernelSubobject	—	kernel.lift_ι
kernelSubobject_factors_iff 📖	mathematical	—	CategoryTheory.Subobject.Factors kernelSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	—	CategoryTheory.Subobject.factorThru_arrow CategoryTheory.Category.assoc kernelSubobject_arrow_comp comp_zero kernelSubobject_factors
kernelSubobject_zero 📖	mathematical	—	kernelSubobject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasEqualizer_of_self Top.top CategoryTheory.Subobject OrderTop.toTop Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.orderTop	—	hasEqualizer_of_self equalizerSubobject_of_self
kernel_map_comp_kernelSubobjectIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject kernel.map CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.w CategoryTheory.Iso.inv kernelSubobjectIso kernelSubobjectMap	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.CommaMorphism.w CategoryTheory.Category.assoc kernelSubobject_arrow' kernel.lift_ι kernelSubobjectMap_arrow kernelSubobject_arrow'_assoc
kernel_map_comp_kernelSubobjectIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel kernel.map CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.w CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying kernelSubobject CategoryTheory.Iso.inv kernelSubobjectIso kernelSubobjectMap	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernel_map_comp_kernelSubobjectIso_inv
le_kernelSubobject 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Subobject.arrow Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	Preorder.toLE kernelSubobject	—	CategoryTheory.Subobject.le_mk_of_comm kernel.lift_ι
pullback_equalizer 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback equalizerSubobject CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasEqualizer_precomp_of_hasEqualizer hasLimitOfHasLimitsOfShape WalkingCospan WidePullbackShape.category WalkingPair cospan equalizer equalizer.ι	—	CategoryTheory.Subobject.skeletal hasEqualizer_precomp_of_hasEqualizer hasLimitOfHasLimitsOfShape Preorder.subsingleton_hom equalizerSubobject_factors CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Subobject.isPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' equalizerSubobject_arrow_comp pullback_factors
pullback_factors 📖	mathematical	CategoryTheory.Subobject.Factors CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback	—	CategoryTheory.Subobject.factorThru_arrow CategoryTheory.Subobject.factors_iff CategoryTheory.Subobject.isPullback CategoryTheory.IsPullback.lift_snd
pullback_factors_iff 📖	mathematical	—	CategoryTheory.Subobject.Factors CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Subobject.factors_iff CategoryTheory.Category.assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Subobject.isPullback CategoryTheory.Subobject.factorThru_arrow_assoc pullback_factors

---

← Back to Index