Subobject 📖 | CompOp | 272 mathmath: IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, 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, Subobject.inf_eq_of_isDetecting, 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, Subobject.wideCospan_map_term, 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.nontrivial_of_not_isZero, Subobject.prod_eq_inf, instWellFoundedGTSubobjectOfIsNoetherianObject, Subobject.finset_sup_factors, Subobject.presheaf_obj, Classifier.SubobjectRepresentableBy.homEquiv_eq, imageToKernel_comp_right, imageToKernel_comp_hom_inv_comp, Limits.factorThruKernelSubobject_comp_arrow, ShortComplex.Exact.isIso_imageToKernel, 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', 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.functor_obj, 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, WellPowered.subobject_small, 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, small_subobject, ExtremalEpi.subobject_eq_top, Subobject.inf_factors, 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.finset_inf_factors, 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, Subobject.subsingleton_of_isZero, 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, 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, instNontrivialSubobjectOfSimple, Limits.equalizerSubobject_arrow_assoc, Subobject.isIso_arrow_iff_eq_top, Subfunctor.orderIsoSubobject_symm_apply, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, 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.subsingleton_of_isInitial, 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, Subobject.sup_factors_of_factors_left, 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.sup_factors_of_factors_right, 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, essentiallySmall_monoOver_iff_small_subobject, Limits.kernelSubobjectMap_id, Limits.kernelSubobject_zero
|