Basic

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

Statistics

Metric	Count
Definitions arrow, equivMonoOver, exists, existsCompRepresentativeIso, existsIsoImage, existsPullbackAdj, imageFactorisation, instCoeOut, isoOfEq, isoOfEqMk, isoOfMkEq, isoOfMkEqMk, lower, lowerAdjunction, lowerCompRepresentativeIso, lowerEquivalence, lower₂, map, mapIso, mapIsoToOrderIso, mapPullbackAdj, mk, ofLE, ofLEMk, ofMkLE, ofMkLEMk, pullback, pullbackπ, representative, representativeIso, underlying, underlyingIso, instPartialOrderSubobject	33
Theorems ext, ext_iff, isIso_hom_left_iff_subobjectMk_eq, isIso_iff_subobjectMk_eq, isIso_left_iff_subobjectMk_eq, subobjectMk_le_mk_of_hom, arrow_congr, arrow_mono, eq_mk_of_comm, eq_of_comm, eq_of_comp_arrow_eq, eq_of_comp_arrow_eq_iff, exists_iso_map, hasColimitsOfSize, hasFiniteLimits, hasLimitsOfShape, hasLimitsOfSize, imageFactorisation_F_I, imageFactorisation_F_m, ind, ind₂, instFaithfulPullback, instIsEquivalenceMonoOverRepresentative, instMonoOfLE, instMonoOfLEMk, instMonoOfMkLE, instMonoOfMkLEMk, isPullback, isPullback_aux, isoOfEqMk_hom, isoOfEqMk_inv, isoOfEq_hom, isoOfEq_inv, isoOfMkEqMk_hom, isoOfMkEqMk_inv, isoOfMkEq_hom, isoOfMkEq_inv, le_mk_of_comm, le_of_comm, lift_mk, lowerEquivalence_counitIso, lowerEquivalence_functor, lowerEquivalence_inverse, lowerEquivalence_unitIso, lower_comm, lower_iso, mapIsoToOrderIso_apply, mapIsoToOrderIso_symm_apply, map_comp, map_id, map_mk, map_obj_injective, map_pullback, mk_arrow, mk_eq_mk_of_comm, mk_eq_of_comm, mk_le_mk_of_comm, mk_le_of_comm, mk_lt_mk_iff_of_comm, mk_lt_mk_of_comm, mk_surjective, ofLEMk_comp, ofLEMk_comp_ofMkLE, ofLEMk_comp_ofMkLEMk, ofLEMk_comp_ofMkLEMk_assoc, ofLEMk_comp_ofMkLE_assoc, ofLE_arrow, ofLE_arrow_assoc, ofLE_comp_ofLE, ofLE_comp_ofLEMk, ofLE_comp_ofLEMk_assoc, ofLE_comp_ofLE_assoc, ofLE_mk_le_mk_of_comm, ofLE_refl, ofMkLEMk_comp, ofMkLEMk_comp_ofMkLE, ofMkLEMk_comp_ofMkLEMk, ofMkLEMk_comp_ofMkLEMk_assoc, ofMkLEMk_comp_ofMkLE_assoc, ofMkLEMk_refl, ofMkLE_arrow, ofMkLE_comp_ofLE, ofMkLE_comp_ofLEMk, ofMkLE_comp_ofLEMk_assoc, ofMkLE_comp_ofLE_assoc, pullback_comp, pullback_id, pullback_map_self, pullback_obj, pullback_obj_mk, representative_arrow, representative_coe, skeletal, underlyingIso_arrow, underlyingIso_arrow_apply, underlyingIso_arrow_assoc, underlyingIso_hom_comp_eq_mk, underlyingIso_hom_comp_eq_mk_assoc, underlying_arrow, underlying_arrow_assoc	100
Total	133

CategoryTheory

Definitions

Name	Category	Theorems
instPartialOrderSubobject 📖	CompOp	257 math math: Classifier.pullback_χ_obj_mk_truth, Limits.kernelSubobjectMap_arrow_assoc, Subobject.map_mk, Limits.imageSubobject_arrow_assoc, Subobject.factorThru_right, Subobject.factors_iff, Limits.imageSubobjectCompIso_hom_arrow, Subobject.underlyingIso_hom_comp_eq_mk_assoc, Subobject.imageFactorisation_F_m, Subobject.underlyingIso_arrow_assoc, Subobject.hasColimitsOfSize, Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀, AlgebraicTopology.NormalizedMooreComplex.obj_d, Dial.tensorObjImpl_rel, imageToKernel_unop, Limits.equalizerSubobject_arrow'_assoc, Subobject.inf_le_left, Subobject.map_comp, imageToKernel'_kernelSubobjectIso, Subobject.isPullback_aux, instIsSimpleOrderSubobjectOfSimple, Limits.kernelSubobject_arrow'_apply, Subobject.factorThru_eq_zero, Subobject.ofMkLEMk_comp_ofMkLEMk_assoc, Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp, isArtinianObject_iff_not_strictAnti, Subobject.top_arrow_isIso, IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, Regular.frobeniusStrongEpiMonoFactorisation_I, Limits.kernelSubobjectIsoComp_hom_arrow, Limits.imageSubobject_arrow_comp_eq_zero, Subobject.map_top, imageToKernel_op, factorThruImageSubobject_comp_imageToKernel, Subobject.inf_comp_left, Limits.kernelSubobject_arrow_assoc, Subobject.bot_eq_initial_to, Limits.kernelSubobjectMap_comp, Limits.kernelSubobject_comp_mono_isIso, Subobject.mk_lt_mk_of_comm, Subobject.inf_arrow_factors_right, Limits.equalizerSubobject_arrow_comp, Subobject.prod_eq_inf, instWellFoundedGTSubobjectOfIsNoetherianObject, Classifier.SubobjectRepresentableBy.homEquiv_eq, imageToKernel_comp_right, imageToKernel_comp_hom_inv_comp, Limits.factorThruKernelSubobject_comp_arrow, ShortComplex.Exact.isIso_imageToKernel, Subobject.sInf_le, not_strictMono_of_isNoetherianObject, Subobject.factorThru_mk_self, imageToKernel_arrow_assoc, Abelian.subobjectIsoSubobjectOp_apply, ShortComplex.exact_iff_isIso_imageToKernel, Subobject.mk_le_mk_of_comm, Dial.comp_le_lemma, simple_iff_subobject_isSimpleOrder, IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, Subobject.bot_factors_iff_zero, Subobject.pullback_id, Limits.factorThruImageSubobject_comp_self_assoc, Subobject.pullback_obj, Subobject.map_pullback, Subobject.inf_eq_map_pullback', Subobject.le_sSup, imageToKernel_epi_comp, Subobject.mapIsoToOrderIso_apply, Classifier.χ_pullback_obj_mk_truth_arrow, Subobject.factorThru_arrow_assoc, Limits.kernelSubobjectIso_comp_kernel_map, Limits.pullback_factors_iff, Subobject.arrow_mono, Subobject.isIso_top_arrow, Subobject.hasLimitsOfShape, Subobject.factors_comp_arrow, Limits.imageSubobjectIso_comp_image_map, Subobject.factors_self, Limits.imageSubobject_zero_arrow, Limits.imageSubobject_zero, subobject_simple_iff_isAtom, Limits.kernelSubobjectIsoComp_inv_arrow, Subobject.map_bot, Classifier.SubobjectRepresentableBy.isPullback, Limits.imageSubobject_le_mk, Subobject.factorThru_add_sub_factorThru_right, Subobject.mk_eq_bot_iff_zero, Subobject.isoOfEq_hom, Subobject.lower_comm, imageToKernel_arrow, antitone_chain_condition_of_isArtinianObject, Limits.kernelOrderHom_coe, Subobject.inf_isPullback, image_le_kernel, Subobject.mk_arrow, Limits.imageSubobject_arrow_comp_apply, Subobject.isoOfEqMk_inv, ObjectProperty.IsStrongGenerator.subobject_eq_top, Limits.kernelSubobject_arrow_comp_apply, Subobject.isoOfMkEq_inv, Subobject.underlyingIso_arrow, Subfunctor.orderIsoSubobject_apply, Dial.Hom.le, imageToKernel_epi_of_zero_of_mono, Limits.kernelSubobjectIso_comp_kernel_map_assoc, Subobject.instIsEquivalenceMonoOverRepresentative, monotone_chain_condition_of_isNoetherianObject, imageToKernel_comp_left, Subobject.ofMkLEMk_comp_ofMkLEMk, Subobject.eq_of_comp_arrow_eq_iff, Limits.imageSubobjectCompIso_inv_arrow_assoc, Regular.instIsRegularEpiFrobeniusMorphism, Limits.imageSubobjectMap_arrow, Limits.imageSubobjectMap_arrow_assoc, Limits.kernelSubobject_arrow, isNoetherianObject_iff_monotone_chain_condition, Subobject.ofLE_refl, Regular.frobeniusStrongEpiMonoFactorisation_e, Subobject.ofMkLEMk_refl, ExtremalEpi.subobject_eq_top, Limits.imageSubobject_comp_le, AlgebraicTopology.NormalizedMooreComplex.d_squared, imageSubobjectIso_imageToKernel', Subobject.mk_lt_mk_iff_of_comm, Limits.imageSubobject_arrow, Limits.imageSubobject_comp_le_epi_of_epi, Dial.tensorUnit_rel, Subobject.imageFactorisation_F_I, Subobject.inf_map, instMonoImageToKernel, Classifier.SubobjectRepresentableBy.iso_inv_left_π_assoc, IsGrothendieckAbelian.generatingMonomorphisms.lt_largerSubobject, Limits.equalizerSubobject_arrow, Limits.imageSubobject_arrow_comp_assoc, Limits.isIso_kernelSubobject_zero_arrow, Subobject.bot_arrow, AlgebraicTopology.NormalizedMooreComplex.map_f, Subobject.lowerEquivalence_counitIso, IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, Subobject.mk_eq_top_of_isIso, Limits.pullback_factors, Subobject.factorThru_add_sub_factorThru_left, Regular.exists_inf_pullback_eq_exists_inf, Subobject.inf_def, Subobject.bot_eq_zero, Subobject.isoOfMkEq_hom, Subobject.top_eq_id, Limits.kernel_map_comp_kernelSubobjectIso_inv, Subobject.skeletal, Subobject.pullback_map_self, Limits.imageSubobject_arrow'_assoc, Subobject.factorThru_arrow, Subobject.inf_arrow_factors_left, Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, Subobject.isoOfEq_inv, Subobject.mapIsoToOrderIso_symm_apply, isArtinianObject_iff_antitone_chain_condition, Subobject.factorThru_add, Limits.equalizerSubobject_of_self, Limits.imageSubobjectCompIso_hom_arrow_assoc, Regular.frobeniusMorphism_isPullback, Subobject.lowerEquivalence_unitIso, imageToKernel_arrow_apply, Subobject.top_factors, ShortComplex.exact_iff_epi_imageToKernel, MonoOver.subobjectMk_le_mk_of_hom, Subobject.eq_top_of_isIso_arrow, Limits.equalizerSubobject_arrow', Subobject.underlying_arrow_assoc, IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, Subobject.pullback_obj_mk, Limits.equalizerSubobject_arrow_comp_assoc, Limits.kernelSubobject_arrow'_assoc, imageToKernel_zero_right, instWellFoundedLTSubobjectOfIsArtinianObject, Subobject.underlyingIso_inv_top_arrow_assoc, Subobject.isPullback, AlgebraicTopology.NormalizedMooreComplex.obj_X, Limits.equalizerSubobject_arrow_assoc, Subobject.isIso_arrow_iff_eq_top, Subfunctor.orderIsoSubobject_symm_apply, Subobject.ofLE_mk_le_mk_of_comm, exists_simple_subobject, Subobject.underlyingIso_inv_top_arrow, Classifier.SubobjectRepresentableBy.iso_inv_left_comp, Subobject.inf_le_right, Subobject.underlyingIso_top_hom, Subfunctor.range_subobjectMk_ι, AlgebraicTopology.NormalizedMooreComplex.objX_zero, Regular.frobeniusStrongEpiMonoFactorisation_m, Classifier.SubobjectRepresentableBy.iso_inv_left_π, Subobject.arrow_congr, Subobject.inf_comp_left_assoc, Subobject.pullback_top, Subobject.epi_iff_mk_eq_top, StructuredArrow.projectSubobject_factors, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.pullback_comp, Limits.imageSubobjectCompIso_inv_arrow, Subobject.isIso_iff_mk_eq_top, Limits.kernelSubobject_arrow_comp_assoc, Subobject.pullback_self, Limits.image_map_comp_imageSubobjectIso_inv, IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, Subobject.inf_comp_right, Subobject.representative_coe, Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc, Limits.kernelSubobject_arrow_apply, Subobject.inf_eq_map_pullback, Limits.imageSubobject_arrow_comp, Subfunctor.Subpresheaf.subobjectMk_range_arrow, imageToKernel_zero_left, Subobject.inf_pullback, Subobject.inf_comp_right_assoc, Subobject.lowerEquivalence_inverse, Subobject.lowerEquivalence_functor, Subfunctor.Subpresheaf.range_subobjectMk_ι, IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_top, Subobject.functor_map, imageToKernel_epi_of_epi_of_zero, IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject, Subobject.finset_inf_arrow_factors, CostructuredArrow.projectQuotient_factors, Limits.kernelSubobject_arrow_comp, Subobject.map_obj_injective, isNoetherianObject_iff_not_strictMono, IsGrothendieckAbelian.generatingMonomorphisms.le_largerSubobject, Limits.factorThruKernelSubobject_comp_kernelSubobjectIso, CostructuredArrow.unop_left_comp_underlyingIso_hom_unop, Subobject.instFaithfulPullback, Subobject.underlyingIso_arrow_apply, Dial.tensorUnitImpl_rel, Abelian.subobjectIsoSubobjectOp_symm_apply, Subobject.underlying_arrow, Limits.cokernelOrderHom_coe, Subobject.representative_arrow, Limits.kernelSubobjectMap_arrow, ModuleCat.toKernelSubobject_arrow, Limits.imageSubobject_arrow', Subobject.factorThru_zero, imageToKernel_comp_mono, Subobject.isoOfEqMk_hom, Limits.kernelSubobject_arrow', Limits.instEpiFactorThruImageSubobjectOfHasEqualizers, Subobject.hasLimitsOfSize, Limits.factorThruImageSubobject_comp_self, Limits.kernelSubobject_comp_le, Subfunctor.subobjectMk_range_arrow, Dial.tensorObj_rel, Subobject.hasFiniteLimits, Subobject.map_id, Limits.kernelSubobjectMap_arrow_apply, Subobject.presheaf_map, not_strictAnti_of_isArtinianObject, Limits.pullback_equalizer, Limits.kernelSubobjectMap_id, Limits.kernelSubobject_zero

CategoryTheory.Comma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	left right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj hom	—	—	—
ext_iff 📖	mathematical	—	left right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj hom	—	ext

CategoryTheory.MonoOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_hom_left_iff_subobjectMk_eq 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom mono	—	mono CategoryTheory.Subobject.mk_eq_mk_of_comm CategoryTheory.Over.w Eq.le CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.Subobject.ofMkLEMk_comp CategoryTheory.Category.id_comp
isIso_iff_subobjectMk_eq 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom mono	—	mono isIso_iff_isIso_hom_left isIso_hom_left_iff_subobjectMk_eq
isIso_left_iff_subobjectMk_eq 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom mono	—	isIso_hom_left_iff_subobjectMk_eq
subobjectMk_le_mk_of_hom 📖	mathematical	—	CategoryTheory.Subobject CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Comma.left CategoryTheory.Comma.hom mono	—	CategoryTheory.Subobject.mk_le_mk_of_comm mono CategoryTheory.Over.w

CategoryTheory.Subobject

Definitions

Name	Category	Theorems
arrow 📖	CompOp	106 math math: CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc, CategoryTheory.Limits.imageSubobject_arrow_assoc, CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow, underlyingIso_hom_comp_eq_mk_assoc, imageFactorisation_F_m, underlyingIso_arrow_assoc, ofLE_arrow, AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.Limits.equalizerSubobject_arrow'_assoc, isPullback_aux, CategoryTheory.Limits.kernelSubobject_arrow'_apply, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp, top_arrow_isIso, wideCospan_map_term, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow, CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero, ofMkLE_arrow, ofLE_arrow_assoc, inf_comp_left, CategoryTheory.Limits.kernelSubobject_arrow_assoc, inf_arrow_factors_right, CategoryTheory.Limits.equalizerSubobject_arrow_comp, ofLEMk_comp, CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow, imageToKernel_arrow_assoc, pullback_obj, CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow, factorThru_arrow_assoc, arrow_mono, isIso_top_arrow, factors_comp_arrow, factors_self, CategoryTheory.Limits.imageSubobject_zero_arrow, CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow, CategoryTheory.Classifier.SubobjectRepresentableBy.isPullback, imageToKernel_arrow, inf_isPullback, mk_arrow, CategoryTheory.Limits.imageSubobject_arrow_comp_apply, CategoryTheory.Limits.kernelSubobject_arrow_comp_apply, underlyingIso_arrow, eq_of_comp_arrow_eq_iff, CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc, CategoryTheory.Limits.imageSubobjectMap_arrow, CategoryTheory.Limits.imageSubobjectMap_arrow_assoc, CategoryTheory.Limits.kernelSubobject_arrow, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, CategoryTheory.Limits.imageSubobject_arrow, imageFactorisation_F_I, CategoryTheory.Limits.equalizerSubobject_arrow, CategoryTheory.Limits.imageSubobject_arrow_comp_assoc, CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow, bot_arrow, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, CategoryTheory.Limits.imageSubobject_arrow'_assoc, factorThru_arrow, inf_arrow_factors_left, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc, CategoryTheory.Regular.frobeniusMorphism_isPullback, imageToKernel_arrow_apply, CategoryTheory.Limits.equalizerSubobject_arrow', underlying_arrow_assoc, CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc, CategoryTheory.Limits.kernelSubobject_arrow'_assoc, imageToKernel_zero_right, underlyingIso_inv_top_arrow_assoc, isPullback, CategoryTheory.Limits.equalizerSubobject_arrow_assoc, isIso_arrow_iff_eq_top, CategoryTheory.Subfunctor.orderIsoSubobject_symm_apply, underlyingIso_inv_top_arrow, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp, underlyingIso_top_hom, CategoryTheory.Subfunctor.range_subobjectMk_ι, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, arrow_congr, leInfCone_π_app_none, inf_comp_left_assoc, CategoryTheory.StructuredArrow.projectSubobject_factors, underlyingIso_hom_comp_eq_mk, CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow, CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, inf_comp_right, CategoryTheory.Limits.kernelSubobject_arrow_apply, CategoryTheory.Limits.imageSubobject_arrow_comp, CategoryTheory.Subfunctor.Subpresheaf.subobjectMk_range_arrow, inf_comp_right_assoc, CategoryTheory.Subfunctor.Subpresheaf.range_subobjectMk_ι, finset_inf_arrow_factors, AlgebraicTopology.inclusionOfMooreComplexMap_f, CategoryTheory.CostructuredArrow.projectQuotient_factors, CategoryTheory.Limits.kernelSubobject_arrow_comp, CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop, underlyingIso_arrow_apply, underlying_arrow, representative_arrow, CategoryTheory.Limits.kernelSubobjectMap_arrow, ModuleCat.toKernelSubobject_arrow, CategoryTheory.Limits.imageSubobject_arrow', CategoryTheory.Limits.kernelSubobject_arrow', CategoryTheory.Subfunctor.subobjectMk_range_arrow, CategoryTheory.Limits.kernelSubobjectMap_arrow_apply
equivMonoOver 📖	CompOp	—
exists 📖	CompOp	8 math math: imageFactorisation_F_m, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, exists_iso_map, CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism, imageFactorisation_F_I, CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf, CategoryTheory.Regular.frobeniusMorphism_isPullback, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m
existsCompRepresentativeIso 📖	CompOp	—
existsIsoImage 📖	CompOp	—
existsPullbackAdj 📖	CompOp	—
imageFactorisation 📖	CompOp	3 math math: imageFactorisation_F_m, imageFactorisation_F_I, CategoryTheory.Regular.frobeniusMorphism_isPullback
instCoeOut 📖	CompOp	—
isoOfEq 📖	CompOp	3 math math: isoOfEq_hom, isoOfEq_inv, imageToKernel_comp_mono
isoOfEqMk 📖	CompOp	2 math math: isoOfEqMk_inv, isoOfEqMk_hom
isoOfMkEq 📖	CompOp	2 math math: isoOfMkEq_inv, isoOfMkEq_hom
isoOfMkEqMk 📖	CompOp	2 math math: isoOfMkEqMk_hom, isoOfMkEqMk_inv
lower 📖	CompOp	6 math math: lower_iso, lower_comm, lowerEquivalence_counitIso, lowerEquivalence_unitIso, lowerEquivalence_inverse, lowerEquivalence_functor
lowerAdjunction 📖	CompOp	—
lowerCompRepresentativeIso 📖	CompOp	—
lowerEquivalence 📖	CompOp	4 math math: lowerEquivalence_counitIso, lowerEquivalence_unitIso, lowerEquivalence_inverse, lowerEquivalence_functor
lower₂ 📖	CompOp	—
map 📖	CompOp	14 math math: map_mk, map_comp, map_top, exists_iso_map, map_pullback, inf_eq_map_pullback', mapIsoToOrderIso_apply, map_bot, inf_map, pullback_map_self, mapIsoToOrderIso_symm_apply, inf_eq_map_pullback, map_obj_injective, map_id
mapIso 📖	CompOp	—
mapIsoToOrderIso 📖	CompOp	2 math math: mapIsoToOrderIso_apply, mapIsoToOrderIso_symm_apply
mapPullbackAdj 📖	CompOp	—
mk 📖	CompOp	—
ofLE 📖	CompOp	31 math math: ofLE_arrow, ofLE_arrow_assoc, inf_comp_left, CategoryTheory.Limits.kernelSubobject_comp_mono_isIso, ofLE_comp_ofLEMk_assoc, imageToKernel_comp_right, ofLEMk_comp_ofMkLE, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, imageToKernel_epi_comp, instMonoOfLE, subobject_ofLE_as_imageToKernel, isoOfEq_hom, inf_isPullback, ofLE_comp_ofLE_assoc, imageToKernel_comp_left, ofLE_refl, CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi, factorThru_ofLE, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, ofLE_comp_ofLEMk, isoOfEq_inv, CategoryTheory.Regular.frobeniusMorphism_isPullback, ofLE_comp_ofLE, ofMkLE_comp_ofLE, ofLE_mk_le_mk_of_comm, ofMkLE_comp_ofLE_assoc, inf_comp_left_assoc, inf_comp_right, ofLEMk_comp_ofMkLE_assoc, inf_comp_right_assoc, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject
ofLEMk 📖	CompOp	12 math math: ofLEMk_comp_ofMkLEMk, ofMkLE_comp_ofLEMk_assoc, ofLE_comp_ofLEMk_assoc, ofLEMk_comp, ofLEMk_comp_ofMkLE, isoOfMkEq_inv, instMonoOfLEMk, ofMkLE_comp_ofLEMk, ofLEMk_comp_ofMkLEMk_assoc, ofLE_comp_ofLEMk, ofLEMk_comp_ofMkLE_assoc, isoOfEqMk_hom
ofMkLE 📖	CompOp	12 math math: ofMkLEMk_comp_ofMkLE, ofMkLE_arrow, ofMkLE_comp_ofLEMk_assoc, ofMkLEMk_comp_ofMkLE_assoc, ofLEMk_comp_ofMkLE, isoOfEqMk_inv, ofMkLE_comp_ofLEMk, instMonoOfMkLE, isoOfMkEq_hom, ofMkLE_comp_ofLE, ofMkLE_comp_ofLE_assoc, ofLEMk_comp_ofMkLE_assoc
ofMkLEMk 📖	CompOp	14 math math: ofMkLEMk_comp_ofMkLEMk_assoc, ofLEMk_comp_ofMkLEMk, ofMkLEMk_comp_ofMkLE, CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop, ofMkLE_comp_ofLEMk_assoc, ofMkLEMk_comp_ofMkLE_assoc, ofMkLEMk_comp, ofMkLE_comp_ofLEMk, ofMkLEMk_comp_ofMkLEMk, ofMkLEMk_refl, ofLEMk_comp_ofMkLEMk_assoc, isoOfMkEqMk_hom, instMonoOfMkLEMk, isoOfMkEqMk_inv
pullback 📖	CompOp	38 math math: CategoryTheory.Classifier.pullback_χ_obj_mk_truth, CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀, CategoryTheory.Dial.tensorObjImpl_rel, isPullback_aux, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, CategoryTheory.Classifier.SubobjectRepresentableBy.homEquiv_eq, CategoryTheory.Dial.comp_le_lemma, pullback_id, pullback_obj, map_pullback, inf_eq_map_pullback', CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow, CategoryTheory.Limits.pullback_factors_iff, CategoryTheory.Dial.Hom.le, CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π_assoc, CategoryTheory.Limits.pullback_factors, CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf, pullback_map_self, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, CategoryTheory.Regular.frobeniusMorphism_isPullback, pullback_obj_mk, isPullback, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π, pullback_top, pullback_comp, pullback_self, inf_eq_map_pullback, inf_pullback, functor_map, instFaithfulPullback, CategoryTheory.Dial.tensorObj_rel, Subobject.presheaf_map, CategoryTheory.Limits.pullback_equalizer
pullbackπ 📖	CompOp	3 math math: CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π_assoc, isPullback, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π
representative 📖	CompOp	9 math math: factors_iff, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp, instIsEquivalenceMonoOverRepresentative, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π_assoc, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π, representative_coe, representative_arrow
representativeIso 📖	CompOp	—
underlying 📖	CompOp	173 math math: CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc, CategoryTheory.Limits.imageSubobject_arrow_assoc, factorThru_right, CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow, underlyingIso_hom_comp_eq_mk_assoc, imageFactorisation_F_m, underlyingIso_arrow_assoc, ofLE_arrow, AlgebraicTopology.NormalizedMooreComplex.obj_d, imageToKernel_unop, CategoryTheory.Limits.equalizerSubobject_arrow'_assoc, imageToKernel'_kernelSubobjectIso, isPullback_aux, CategoryTheory.Limits.kernelSubobject_arrow'_apply, factorThru_eq_zero, ofLEMk_comp_ofMkLEMk, ofMkLEMk_comp_ofMkLE, top_arrow_isIso, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow, CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero, ofMkLE_arrow, imageToKernel_op, factorThruImageSubobject_comp_imageToKernel, ofLE_arrow_assoc, ofMkLE_comp_ofLEMk_assoc, inf_comp_left, CategoryTheory.Limits.kernelSubobject_arrow_assoc, ofMkLEMk_comp_ofMkLE_assoc, CategoryTheory.Limits.kernelSubobjectMap_comp, CategoryTheory.Limits.kernelSubobject_comp_mono_isIso, inf_arrow_factors_right, CategoryTheory.Limits.equalizerSubobject_arrow_comp, ofLE_comp_ofLEMk_assoc, ofLEMk_comp, imageToKernel_comp_right, imageToKernel_comp_hom_inv_comp, CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel, factorThru_mk_self, ofLEMk_comp_ofMkLE, imageToKernel_arrow_assoc, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc, pullback_obj, imageToKernel_epi_comp, instMonoOfLE, CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow, factorThru_arrow_assoc, CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map, arrow_mono, isIso_top_arrow, factors_comp_arrow, CategoryTheory.Limits.imageSubobjectIso_comp_image_map, factors_self, CategoryTheory.Limits.imageSubobject_zero_arrow, CategoryTheory.subobject_simple_iff_isAtom, CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow, CategoryTheory.Classifier.SubobjectRepresentableBy.isPullback, factorThru_add_sub_factorThru_right, isoOfEq_hom, imageToKernel_arrow, inf_isPullback, mk_arrow, CategoryTheory.Limits.imageSubobject_arrow_comp_apply, isoOfEqMk_inv, CategoryTheory.Limits.kernelSubobject_arrow_comp_apply, isoOfMkEq_inv, underlyingIso_arrow, ofLE_comp_ofLE_assoc, instMonoOfLEMk, imageToKernel_epi_of_zero_of_mono, CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc, ofMkLE_comp_ofLEMk, imageToKernel_comp_left, eq_of_comp_arrow_eq_iff, CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc, CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism, CategoryTheory.Limits.imageSubobjectMap_arrow, CategoryTheory.Limits.imageSubobjectMap_arrow_assoc, CategoryTheory.Limits.kernelSubobject_arrow, ofLE_refl, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, ofLEMk_comp_ofMkLEMk_assoc, AlgebraicTopology.NormalizedMooreComplex.d_squared, imageSubobjectIso_imageToKernel', CategoryTheory.Limits.imageSubobject_arrow, CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi, imageFactorisation_F_I, instMonoImageToKernel, factorThru_ofLE, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π_assoc, CategoryTheory.Limits.equalizerSubobject_arrow, instMonoOfMkLE, CategoryTheory.Limits.imageSubobject_arrow_comp_assoc, CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow, bot_arrow, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, ofLE_comp_ofLEMk, factorThru_add_sub_factorThru_left, isoOfMkEq_hom, CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv, CategoryTheory.Limits.imageSubobject_arrow'_assoc, factorThru_arrow, inf_arrow_factors_left, isoOfEq_inv, factorThru_add, CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc, CategoryTheory.Regular.frobeniusMorphism_isPullback, imageToKernel_arrow_apply, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel, CategoryTheory.Limits.equalizerSubobject_arrow', underlying_arrow_assoc, ofLE_comp_ofLE, CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc, ofMkLE_comp_ofLE, CategoryTheory.Limits.kernelSubobject_arrow'_assoc, imageToKernel_zero_right, underlyingIso_inv_top_arrow_assoc, isPullback, AlgebraicTopology.NormalizedMooreComplex.obj_X, CategoryTheory.Limits.equalizerSubobject_arrow_assoc, isIso_arrow_iff_eq_top, CategoryTheory.Subfunctor.orderIsoSubobject_symm_apply, ofLE_mk_le_mk_of_comm, CategoryTheory.exists_simple_subobject, underlyingIso_inv_top_arrow, underlyingIso_top_hom, ofMkLE_comp_ofLE_assoc, CategoryTheory.Subfunctor.range_subobjectMk_ι, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π, arrow_congr, inf_comp_left_assoc, CategoryTheory.StructuredArrow.projectSubobject_factors, underlyingIso_hom_comp_eq_mk, CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow, CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc, CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, inf_comp_right, ofLEMk_comp_ofMkLE_assoc, representative_coe, CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc, CategoryTheory.Limits.kernelSubobject_arrow_apply, CategoryTheory.Limits.imageSubobject_arrow_comp, CategoryTheory.Subfunctor.Subpresheaf.subobjectMk_range_arrow, imageToKernel_zero_left, inf_comp_right_assoc, CategoryTheory.Subfunctor.Subpresheaf.range_subobjectMk_ι, imageToKernel_epi_of_epi_of_zero, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject, finset_inf_arrow_factors, CategoryTheory.CostructuredArrow.projectQuotient_factors, CategoryTheory.Limits.kernelSubobject_arrow_comp, CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso, CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop, underlyingIso_arrow_apply, underlying_arrow, CategoryTheory.Limits.kernelSubobjectMap_arrow, ModuleCat.toKernelSubobject_arrow, CategoryTheory.Limits.imageSubobject_arrow', factorThru_zero, imageToKernel_comp_mono, isoOfEqMk_hom, CategoryTheory.Limits.kernelSubobject_arrow', CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers, CategoryTheory.Limits.factorThruImageSubobject_comp_self, CategoryTheory.Subfunctor.subobjectMk_range_arrow, CategoryTheory.Limits.kernelSubobjectMap_arrow_apply, CategoryTheory.Limits.kernelSubobjectMap_id
underlyingIso 📖	CompOp	11 math math: underlyingIso_hom_comp_eq_mk_assoc, underlyingIso_arrow_assoc, factorThru_mk_self, underlyingIso_arrow, underlyingIso_inv_top_arrow_assoc, ofLE_mk_le_mk_of_comm, underlyingIso_inv_top_arrow, underlyingIso_top_hom, underlyingIso_hom_comp_eq_mk, CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop, underlyingIso_arrow_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrow_congr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Subobject CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	—	CategoryTheory.Category.id_comp
arrow_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	—	CategoryTheory.ObjectProperty.FullSubcategory.property
eq_mk_of_comm 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.hom arrow	—	—	eq_of_comm CategoryTheory.Category.assoc underlyingIso_arrow
eq_of_comm 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.hom arrow	—	—	le_antisymm le_of_comm CategoryTheory.Iso.inv_comp_eq
eq_of_comp_arrow_eq 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	—	—	CategoryTheory.cancel_mono arrow_mono
eq_of_comp_arrow_eq_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	—	eq_of_comp_arrow_eq
exists_iso_map 📖	mathematical	—	exists map	—	lower_iso
hasColimitsOfSize 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.Limits.HasColimitsOfSize CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	CategoryTheory.Limits.hasColimitsOfSize_thinSkeleton CategoryTheory.MonoOver.isThin CategoryTheory.MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	CategoryTheory.Limits.hasLimitsOfShape_thinSkeleton CategoryTheory.MonoOver.isThin CategoryTheory.MonoOver.hasLimitsOfShape
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
imageFactorisation_F_I 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct arrow CategoryTheory.Limits.ImageFactorisation.F imageFactorisation exists	—	—
imageFactorisation_F_m 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct arrow CategoryTheory.Limits.ImageFactorisation.F imageFactorisation exists	—	—
ind 📖	—	—	—	—	Quotient.inductionOn' CategoryTheory.MonoOver.mono
ind₂ 📖	—	—	—	—	Quotient.inductionOn₂' CategoryTheory.MonoOver.mono
instFaithfulPullback 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback	—	Preorder.subsingleton_hom
instIsEquivalenceMonoOverRepresentative 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono representative	—	CategoryTheory.Equivalence.isEquivalence_functor
instMonoOfLE 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.Mono CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE	—	CategoryTheory.eq_whisker eq_of_comp_arrow_eq CategoryTheory.Category.assoc ofLE_arrow
instMonoOfLEMk 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.Mono CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLEMk	—	CategoryTheory.mono_comp instMonoOfLE CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_hom
instMonoOfMkLE 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.Mono CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLE	—	CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv instMonoOfLE
instMonoOfMkLEMk 📖	mathematical	—	CategoryTheory.Mono ofMkLEMk	—	CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv instMonoOfLE CategoryTheory.Iso.isIso_hom
isPullback 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying pullback pullbackπ arrow	—	isPullback_aux
isPullback_aux 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying pullback arrow	—	mk_surjective CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.snd_of_mono arrow_mono pullback_obj CategoryTheory.IsPullback.of_iso CategoryTheory.IsPullback.of_hasPullback CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc underlyingIso_arrow CategoryTheory.Category.id_comp
isoOfEqMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying isoOfEqMk ofLEMk	—	—
isoOfEqMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying isoOfEqMk ofMkLE	—	—
isoOfEq_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying isoOfEq ofLE	—	—
isoOfEq_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying isoOfEq ofLE	—	—
isoOfMkEqMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom isoOfMkEqMk ofMkLEMk	—	—
isoOfMkEqMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv isoOfMkEqMk ofMkLEMk	—	—
isoOfMkEq_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying isoOfMkEq ofMkLE	—	—
isoOfMkEq_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying isoOfMkEq ofLEMk	—	—
le_mk_of_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	Preorder.toLE	—	le_of_comm CategoryTheory.Category.assoc underlyingIso_arrow
le_of_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	Preorder.toLE	—	arrow_mono mk_arrow mk_le_mk_of_comm
lift_mk 📖	mathematical	—	lift	—	—
lowerEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject lowerEquivalence CategoryTheory.eqToIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp lower CategoryTheory.Equivalence.inverse CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Equivalence.functor CategoryTheory.Functor.id	—	—
lowerEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject lowerEquivalence lower CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	—
lowerEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject lowerEquivalence lower CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono	—	—
lowerEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject lowerEquivalence CategoryTheory.eqToIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp lower CategoryTheory.Equivalence.functor CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Equivalence.inverse	—	—
lower_comm 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.ThinSkeleton Preorder.smallCategory CategoryTheory.ThinSkeleton.preorder CategoryTheory.Subobject PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.toThinSkeleton lower	—	—
lower_iso 📖	mathematical	—	lower	—	CategoryTheory.ThinSkeleton.map_iso_eq CategoryTheory.MonoOver.isThin
mapIsoToOrderIso_apply 📖	mathematical	—	DFunLike.coe RelIso CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject RelIso.instFunLike mapIsoToOrderIso CategoryTheory.Functor.obj Preorder.smallCategory map CategoryTheory.Iso.hom	—	—
mapIsoToOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe RelIso CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject RelIso.instFunLike RelIso.symm mapIsoToOrderIso CategoryTheory.Functor.obj Preorder.smallCategory map CategoryTheory.Iso.inv	—	—
map_comp 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.mono_comp	—	Quotient.inductionOn' CategoryTheory.mono_comp
map_id 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.instMonoId	—	Quotient.inductionOn' CategoryTheory.instMonoId
map_mk 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.mono_comp	—	—
map_obj_injective 📖	mathematical	—	CategoryTheory.Subobject CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map	—	ind mk_eq_mk_of_comm CategoryTheory.mono_comp CategoryTheory.cancel_mono CategoryTheory.Category.assoc ofMkLEMk_comp
map_pullback 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject map pullback	—	Quotient.ind' CategoryTheory.ThinSkeleton.equiv_of_both_ways CategoryTheory.MonoOver.isThin CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.lift_snd CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst CategoryTheory.Limits.pullback.lift_snd_assoc CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd
mk_arrow 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow arrow_mono	—	Quotient.inductionOn' arrow_mono Quotient.mk_out' Quotient.sound' CategoryTheory.Category.id_comp
mk_eq_mk_of_comm 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	—	eq_mk_of_comm CategoryTheory.Category.assoc
mk_eq_of_comm 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.hom arrow	—	—	eq_mk_of_comm CategoryTheory.Iso.symm_hom CategoryTheory.Iso.inv_comp_eq
mk_le_mk_of_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	—
mk_le_of_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying arrow	Preorder.toLE	—	le_of_comm CategoryTheory.Category.assoc
mk_lt_mk_iff_of_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Subobject Preorder.toLT PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.IsIso	—	mk_eq_mk_of_comm mk_lt_mk_of_comm
mk_lt_mk_of_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.IsIso	CategoryTheory.Subobject Preorder.toLT PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	LE.le.lt_or_eq mk_le_mk_of_comm CategoryTheory.cancel_mono isoOfMkEqMk_hom ofMkLEMk_comp CategoryTheory.Iso.isIso_hom
mk_surjective 📖	—	—	—	—	arrow_mono mk_arrow
ofLEMk_comp 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLEMk arrow	—	CategoryTheory.Category.assoc ofLE_arrow
ofLEMk_comp_ofMkLE 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLEMk ofMkLE ofLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Functor.map_comp
ofLEMk_comp_ofMkLEMk 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLEMk ofMkLEMk LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Functor.map_comp_assoc
ofLEMk_comp_ofMkLEMk_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLEMk ofMkLEMk LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofLEMk_comp_ofMkLEMk
ofLEMk_comp_ofMkLE_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLEMk ofMkLE ofLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofLEMk_comp_ofMkLE
ofLE_arrow 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE arrow	—	underlying_arrow
ofLE_arrow_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofLE_arrow
ofLE_comp_ofLE 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE LE.le.trans	—	LE.le.trans CategoryTheory.Functor.map_comp
ofLE_comp_ofLEMk 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE ofLEMk LE.le.trans	—	LE.le.trans CategoryTheory.Functor.map_comp_assoc
ofLE_comp_ofLEMk_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE ofLEMk LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofLE_comp_ofLEMk
ofLE_comp_ofLE_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofLE_comp_ofLE
ofLE_mk_le_mk_of_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	ofLE mk_le_mk_of_comm CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.hom underlyingIso CategoryTheory.Iso.inv	—	eq_of_comp_arrow_eq mk_le_mk_of_comm ofLE_arrow CategoryTheory.Category.assoc underlyingIso_arrow
ofLE_refl 📖	mathematical	—	ofLE le_rfl CategoryTheory.Subobject PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying	—	le_rfl CategoryTheory.cancel_mono arrow_mono ofLE_arrow CategoryTheory.Category.id_comp
ofMkLEMk_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ofMkLEMk	—	CategoryTheory.Category.assoc ofLE_arrow underlyingIso_arrow
ofMkLEMk_comp_ofMkLE 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLEMk ofMkLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Functor.map_comp
ofMkLEMk_comp_ofMkLEMk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ofMkLEMk LE.le.trans CategoryTheory.Subobject PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Functor.map_comp_assoc
ofMkLEMk_comp_ofMkLEMk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ofMkLEMk LE.le.trans CategoryTheory.Subobject PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofMkLEMk_comp_ofMkLEMk
ofMkLEMk_comp_ofMkLE_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ofMkLEMk CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofMkLEMk_comp_ofMkLE
ofMkLEMk_refl 📖	mathematical	—	ofMkLEMk le_rfl CategoryTheory.Subobject PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	le_rfl CategoryTheory.cancel_mono ofMkLEMk_comp CategoryTheory.Category.id_comp
ofMkLE_arrow 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLE arrow	—	CategoryTheory.Category.assoc ofLE_arrow underlyingIso_arrow
ofMkLE_comp_ofLE 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLE ofLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp
ofMkLE_comp_ofLEMk 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLE ofLEMk ofMkLEMk LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc
ofMkLE_comp_ofLEMk_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLE ofLEMk ofMkLEMk LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofMkLE_comp_ofLEMk
ofMkLE_comp_ofLE_assoc 📖	mathematical	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory underlying ofMkLE ofLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofMkLE_comp_ofLE
pullback_comp 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	Quotient.inductionOn'
pullback_id 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	Quotient.inductionOn'
pullback_map_self 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback map	—	—
pullback_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback CategoryTheory.Limits.pullback underlying arrow CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd_of_mono arrow_mono	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.snd_of_mono arrow_mono mk_surjective CategoryTheory.IsPullback.of_hasPullback mk_eq_mk_of_comm CategoryTheory.Category.comp_id underlyingIso_arrow CategoryTheory.Category.id_comp CategoryTheory.Limits.pullback.map_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.id CategoryTheory.Limits.limit.lift_π
pullback_obj_mk 📖	mathematical	CategoryTheory.IsPullback	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject pullback	—	CategoryTheory.Iso.to_eq
representative_arrow 📖	mathematical	—	CategoryTheory.MonoOver.arrow CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono representative arrow	—	—
representative_coe 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.MonoOver CategoryTheory.ObjectProperty.FullSubcategory.category representative underlying	—	—
skeletal 📖	mathematical	—	CategoryTheory.Skeletal CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	CategoryTheory.ThinSkeleton.skeletal CategoryTheory.MonoOver.isThin
underlyingIso_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.inv underlyingIso arrow	—	CategoryTheory.Over.w
underlyingIso_arrow_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.ConcreteCategory.hom arrow CategoryTheory.Iso.inv underlyingIso	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise underlyingIso_arrow
underlyingIso_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.inv underlyingIso arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' underlyingIso_arrow
underlyingIso_hom_comp_eq_mk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.hom underlyingIso arrow	—	CategoryTheory.Iso.eq_inv_comp underlyingIso_arrow
underlyingIso_hom_comp_eq_mk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Iso.hom underlyingIso arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
underlying_arrow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Functor.map arrow	—	CategoryTheory.Over.w
underlying_arrow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject underlying CategoryTheory.Functor.map arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' underlying_arrow

---

← Back to Index