Documentation Verification Report

Equalizers

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

Statistics

MetricCount
DefinitionsofCofork, Cofork, desc, desc', homIso, mk, mk', ofExistsUnique, ext, isColimitEquivOfIsos, isColimitOfIsos, isoCoforkOfπ, mkHom, ofCocone, ofπ, π, ext, ofFork, Fork, homIso, lift', mk, mk', ofExistsUnique, equivOfIsos, ext, isLimitEquivOfIsos, isLimitOfIsos, isoForkOfι, mkHom, ofCone, ofι, ι, ext, HasCoequalizer, HasCoequalizers, HasEqualizer, HasEqualizers, WalkingParallelPair, WalkingParallelPairHom, comp, coconeOfIsSplitEpi, coequalizer, cofork, desc, desc', isoTargetOfSelf, π, coequalizerComparison, coequalizerIsCoequalizer, coneOfIsSplitMono, diagramIsoParallelPair, equalizer, fork, isoSourceOfSelf, lift', ι, equalizerComparison, equalizerIsEqualizer, idCofork, idFork, instDecidableEqWalkingParallelPair, instDecidableEqWalkingParallelPairHom, decEq, instInhabitedWalkingParallelPair, default, instInhabitedWalkingParallelPairHomZeroOne, isCoequalizerEpiComp, isColimitIdCofork, isEqualizerCompMono, isLimitIdFork, isLimitPrecompFork, isSplitEpiCoequalizes, isSplitMonoEqualizes, liftPrecomp, parallelPair, eqOfHomEq, ext, parallelPairHom, parallelPairHomMk, parallelPairIso, parallelPairIsoMk, precompFork, splitEpiOfCoequalizer, splitEpiOfIdempotentCoequalizer, splitEpiOfIdempotentOfIsColimitCofork, splitMonoOfEqualizer, splitMonoOfIdempotentEqualizer, splitMonoOfIdempotentOfIsLimitFork, walkingParallelPairHomCategory, walkingParallelPairOp, walkingParallelPairOpEquiv
92
TheoremsofCofork_ι, epi, existsUnique, homIso_apply_coe, homIso_natural, homIso_symm_apply, hom_ext, π_desc, π_desc', π_desc'_assoc, π_desc_assoc, app_one_eq_π, app_zero_eq_comp_π_left, app_zero_eq_comp_π_right, app_zero_eq_comp_π_right_assoc, coequalizer_ext, condition, condition_assoc, ext_hom, ext_inv, mkHom_hom, ofCocone_ι, ofπ_pt, ofπ_ι_app, π_ofπ, π_precompose, ofFork_π, existsUnique, homIso_apply_coe, homIso_natural, homIso_symm_apply, hom_ext, lift_ι, lift_ι', lift_ι'_assoc, lift_ι_assoc, mk_lift, mono, app_one_eq_ι_comp_left, app_one_eq_ι_comp_right, app_one_eq_ι_comp_right_assoc, app_zero_eq_ι, condition, condition_assoc, equalizer_ext, equivOfIsos_functor_obj_ι, equivOfIsos_inverse_obj_ι, ext_hom, ext_inv, hom_comp_ι, hom_comp_ι_assoc, isoForkOfι_hom_hom, isoForkOfι_inv_hom, mkHom_hom, ofCone_π, ofι_pt, ofι_π_app, ι_ofι, ι_postcompose, π_comp_hom, π_comp_hom_assoc, assoc, comp_id, id_comp, coconeOfIsSplitEpi_pt, coconeOfIsSplitEpi_ι_app, coconeOfIsSplitEpi_π, cofork_ι_app_one, cofork_π, condition, condition_assoc, existsUnique, hom_ext, hom_ext_iff, isoTargetOfSelf_hom, isoTargetOfSelf_inv, π_colimMap_desc, π_desc, π_desc_assoc, π_epi, π_of_eq, π_of_self, coequalizerComparison_map_desc, coequalizerComparison_map_desc_assoc, coneOfIsSplitMono_pt, coneOfIsSplitMono_ι, coneOfIsSplitMono_π_app, diagramIsoParallelPair_hom_app, diagramIsoParallelPair_inv_app, epi_of_isColimit_cofork, eq_of_epi_equalizer, eq_of_epi_fork_ι, eq_of_mono_coequalizer, eq_of_mono_cofork_π, condition, condition_assoc, existsUnique, fork_ι, fork_π_app_zero, hom_ext, hom_ext_iff, isoSourceOfSelf_hom, isoSourceOfSelf_inv, lift_ι, lift_ι_assoc, ι_mono, ι_of_eq, ι_of_self, equalizerComparison_comp_π, equalizerComparison_comp_π_assoc, hasCoequalizer_epi_comp, hasCoequalizer_of_self, hasCoequalizers_of_hasColimit_parallelPair, hasEqualizer_comp_mono, hasEqualizer_of_self, hasEqualizer_precomp_of_equalizer, hasEqualizer_precomp_of_hasEqualizer, hasEqualizers_of_hasLimit_parallelPair, isIso_colimit_cocone_parallelPair_of_eq, isIso_colimit_cocone_parallelPair_of_self, isIso_limit_cocone_parallelPair_of_epi, isIso_limit_cone_parallelPair_of_epi, isIso_limit_cone_parallelPair_of_eq, isIso_limit_cone_parallelPair_of_self, map_lift_equalizerComparison, map_lift_equalizerComparison_assoc, mono_of_isLimit_fork, eqOfHomEq_hom_app, eqOfHomEq_inv_app, ext_hom_app, ext_inv_app, parallelPairHomMk_app, parallelPairHom_app_one, parallelPairHom_app_zero, parallelPairIsoMk_hom_app, parallelPairIsoMk_inv_app, parallelPair_functor_obj, parallelPair_map_left, parallelPair_map_right, parallelPair_obj_one, parallelPair_obj_zero, splitEpiOfIdempotentOfIsColimitCofork_section_, splitMonoOfIdempotentOfIsLimitFork_retraction, walkingParallelPairHom_id, walkingParallelPairOpEquiv_counitIso_hom_app_op_one, walkingParallelPairOpEquiv_counitIso_hom_app_op_zero, walkingParallelPairOpEquiv_counitIso_inv_app_op_one, walkingParallelPairOpEquiv_counitIso_inv_app_op_zero, walkingParallelPairOpEquiv_counitIso_one, walkingParallelPairOpEquiv_counitIso_zero, walkingParallelPairOpEquiv_functor, walkingParallelPairOpEquiv_inverse, walkingParallelPairOpEquiv_unitIso_hom_app_one, walkingParallelPairOpEquiv_unitIso_hom_app_zero, walkingParallelPairOpEquiv_unitIso_inv_app_one, walkingParallelPairOpEquiv_unitIso_inv_app_zero, walkingParallelPairOpEquiv_unitIso_one, walkingParallelPairOpEquiv_unitIso_zero, walkingParallelPairOp_left, walkingParallelPairOp_one, walkingParallelPairOp_right, walkingParallelPairOp_zero, ι_comp_coequalizerComparison, ι_comp_coequalizerComparison_assoc
164
Total256

CategoryTheory.Limits

Definitions

NameCategoryTheorems
Cofork 📖CompOp
24 mathmath: MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom, MultispanIndex.ofSigmaCoforkFunctor_obj, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_π, reflexiveCoforkEquivCofork_inverse_obj_pt, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, Cofork.ext_inv, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app, MultispanIndex.toSigmaCoforkFunctor_obj, Cofork.ext_hom, reflexiveCoforkEquivCofork_inverse_obj_π, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse, MultispanIndex.toSigmaCoforkFunctor_map_hom, MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, MultispanIndex.ofSigmaCoforkFunctor_map_hom, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor
Fork 📖CompOp
26 mathmath: MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom, MulticospanIndex.multiforkEquivPiFork_functor_map_hom, Fork.isoForkOfι_hom_hom, MulticospanIndex.toPiForkFunctor_map_hom, Fork.equivOfIsos_functor_obj_ι, MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor, MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι, MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, MulticospanIndex.multiforkEquivPiFork_functor_obj_pt, MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, Fork.ext_hom, Fork.ext_inv, MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app, MulticospanIndex.toPiForkFunctor_obj, Fork.equivOfIsos_inverse_obj_ι, MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, MulticospanIndex.ofPiForkFunctor_obj, MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, MulticospanIndex.ofPiForkFunctor_map_hom, Fork.isoForkOfι_inv_hom, MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι, MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom
HasCoequalizer 📖MathDef
13 mathmath: CategoryTheory.Monad.HasCoequalizerOfIsSplitPair.out, hasCoequalizer_of_hasSplitCoequalizer, hasCoequalizer_of_self, hasReflexiveCoequalizer_iff_hasCoequalizer, CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel, hasCoequalizer_of_common_section, CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair, CategoryTheory.Regular.instHasCoequalizerFstSnd, Multicoequalizer.instHasCoequalizerFstSigmaMapSndSigmaMap, AlgebraicGeometry.LocallyRingedSpace.instHasCoequalizer, hasCoequalizer_epi_comp, HasReflexiveCoequalizers.has_coeq, CategoryTheory.Regular.hasCoequalizer_of_isKernelPair
HasCoequalizers 📖MathDef
9 mathmath: AlgebraicGeometry.LocallyRingedSpace.instHasCoequalizers, hasCoequalizers_opposite, CategoryTheory.Abelian.hasCoequalizers, CategoryTheory.NormalEpiCategory.hasCoequalizers, CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels, hasCoequalizers_of_hasColimit_parallelPair, hasCoequalizers_of_hasPushouts_and_binary_coproducts, hasCoequalizers_of_hasWideCoequalizers, ModuleCat.instHasCoequalizers
HasEqualizer 📖MathDef
12 mathmath: hasEqualizer_of_common_retraction, Multiequalizer.instHasEqualizerFstPiMapSndPiMap, CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair.out, hasEqualizer_of_hasSplitEqualizer, HasCoreflexiveEqualizers.has_eq, hasEqualizer_precomp_of_equalizer, hasEqualizer_of_self, hasEqualizer_precomp_of_hasEqualizer, CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent, CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair, hasEqualizer_comp_mono, CategoryTheory.Preadditive.hasEqualizer_of_hasKernel
HasEqualizers 📖MathDef
11 mathmath: SemiNormedGrp.instHasEqualizers, hasEqualizers_opposite, hasEqualizers_of_hasLimit_parallelPair, CategoryTheory.PreGaloisCategory.instHasEqualizers, hasEqualizers_of_hasPullbacks_and_binary_products, CategoryTheory.Preadditive.hasEqualizers_of_hasKernels, hasEqualizers_of_hasWideEqualizers, CategoryTheory.Over.instHasEqualizers, ωCPO.instHasEqualizers, CategoryTheory.Abelian.hasEqualizers, CategoryTheory.NormalMonoCategory.hasEqualizers
WalkingParallelPair 📖CompData
484 mathmath: Fork.IsLimit.homIso_natural, walkingParallelPairOpEquiv_unitIso_hom_app_zero, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc, cokernelBiproductιIso_hom, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition, MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt, AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg', Fork.IsLimit.lift_ι'_assoc, walkingParallelPairOp_left, map_π_preserves_coequalizer_inv_colimMap, parallelPairOpIso_inv_app_zero, CategoryTheory.Comonad.ComonadicityInternal.unitFork_π_app, Types.coequalizerIso_quot_comp_inv, CategoryTheory.PreOneHypercover.forkOfIsColimit_pt, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg, kernelBiprodSndIso_hom, colimit_ι_zero_cokernel_desc_assoc, Fork.π_comp_hom, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, CategoryTheory.Comonad.beckCoalgebraFork_pt, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app, Bimod.whiskerLeft_hom, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, CategoryTheory.Comonad.ComonadicityInternal.unitFork_pt, CategoryTheory.Functor.PreservesHomology.preservesKernels, MulticospanIndex.multiforkEquivPiFork_functor_map_hom, walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app, walkingParallelPairOpEquiv_counitIso_hom_app_op_one, Fork.unop_ι_app_zero, isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair, KernelFork.condition_assoc, KernelFork.mapOfIsLimit_ι_assoc, Cofork.ofCocone_ι, walkingParallelPairOpEquiv_counitIso_inv_app_op_zero, CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc, Fork.isoForkOfι_hom_hom, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, CategoryTheory.Monad.beckCoequalizer_desc, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc, Fork.IsLimit.mono, kernelForkBiproductToSubtype_cone, KernelFork.IsLimit.isZero_of_mono, CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, cokernelCoforkBiproductFromSubtype_isColimit, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, CategoryTheory.IsSplitCoequalizer.asCofork_pt, PreservesCokernel.of_iso_comparison, AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated, TopCat.coequalizer_isOpen_iff, kernelBiprodFstIso_hom, walkingParallelPairHom_id, of_iso_comparison, AlgebraicGeometry.IsImmersion.instιScheme, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom, closedUnderLimitsOfShape_walkingParallelPair_isIndObject, WalkingParallelPair.inclusionWalkingReflexivePair_map, parallelPairOpIso_inv_app_one, Types.coequalizerIso_π_comp_hom_apply, MulticospanIndex.parallelPairDiagram_map, kernelBiproductπIso_hom, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, Multicofork.ofSigmaCofork_ι_app_right', CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out, Fork.ofι_pt, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.f', equalizerPullbackMapIso_inv_ι_snd, CokernelCofork.π_mapOfIsColimit, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf', Cofork.unop_π_app_one, binaryBiconeOfIsSplitEpiOfKernel_inl, Cofork.IsColimit.epi, CategoryTheory.instHasColimitsOfShapeWalkingParallelPairInd, walkingParallelPairOpEquiv_counitIso_zero, equalizerPullbackMapIso_inv_ι_fst, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, MulticospanIndex.toPiForkFunctor_map_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, map_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, Types.equalizerIso_inv_comp_ι, PreservesEqualizer.of_iso_comparison, Cofork.condition_assoc, Fork.ι_postcompose, Fork.equivOfIsos_functor_obj_ι, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_H, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f, Fork.IsLimit.existsUnique, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, CokernelCofork.IsColimit.isIso_π, equalizerPullbackMapIso_hom_fst_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, Fork.hom_comp_ι, Multicofork.toSigmaCofork_pt, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, CategoryTheory.ShortComplex.RightHomologyData.wι_assoc, Multifork.toPiFork_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, parallelPairOpIso_hom_app_one, preservesKernel_zero, HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair, MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom, Fork.unop_ι_app_one, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι, CategoryTheory.NormalMonoCategory.hasLimit_parallelPair, kernelBiprodFstIso_inv, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, kernelBiproductToSubtypeIso_hom, CokernelCofork.condition, isIso_limit_cone_parallelPair_of_epi, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q, opParallelPairIso_hom_app_zero, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.g, binaryBiconeOfIsSplitMonoOfCokernel_inr, parallelPair_map_left, Fork.IsLimit.homIso_symm_apply, CategoryTheory.Monad.beckAlgebraCofork_pt, Cofork.app_zero_eq_comp_π_left, diagramIsoParallelPair_hom_app, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_H, CommRingCat.Under.instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier, CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer', cokernelBiprodInlIso_inv, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, opParallelPairIso_hom_app_one, Cofork.IsColimit.homIso_apply_coe, coneOfIsSplitMono_π_app, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf, MulticospanIndex.parallelPairDiagram_obj, CommRingCat.instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι, Multicofork.ofSigmaCofork_π, MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, CokernelCofork.mapIsoOfIsColimit_inv, Types.coequalizerIso_quot_comp_inv_apply, Multicofork.ofSigmaCofork_pt, CategoryTheory.Preadditive.forkOfKernelFork_pt, Fork.op_pt, walkingParallelPairOpEquiv_functor, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K, Types.coequalizerIso_π_comp_hom, Fork.ofι_π_app, Cofork.op_π_app_zero, Cofork.IsColimit.π_desc_assoc, MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.out, cokernelBiprodInrIso_inv, ωCPO.instHasLimitWalkingParallelPairParallelPair, MulticospanIndex.multiforkEquivPiFork_functor_obj_pt, walkingParallelFamilyEquivWalkingParallelPair_functor_map, walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app, Fork.hom_comp_ι_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, walkingParallelFamilyEquivWalkingParallelPair_inverse_obj, KernelFork.mapIsoOfIsLimit_inv, Types.equalizerIso_hom_comp_subtype_apply, WalkingParallelPair.inclusionWalkingReflexivePair_obj, MultispanIndex.ofSigmaCoforkFunctor_obj, CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair.out, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, binaryBiconeOfIsSplitMonoOfCokernel_pt, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt, CokernelCofork.mapIsoOfIsColimit_hom, Fork.ofCone_π, π_tensor_id_preserves_coequalizer_inv_desc, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair, KernelFork.IsLimit.isIso_ι, Cofork.π_precompose, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, CategoryTheory.Equalizer.Presieve.sheaf_condition, KernelFork.condition, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel, MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, MulticospanIndex.parallelPairDiagramOfIsLimit_map, Fork.IsLimit.homIso_apply_coe, map_π_preserves_coequalizer_inv_colimMap_assoc, Fork.IsLimit.lift_ι, Multicofork.ofSigmaCofork_ι_app_right, CategoryTheory.Functor.PreservesHomology.preservesCokernels, Types.equalizerIso_hom_comp_subtype, cokernelBiprodInrIso_hom, CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA, CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.g', binaryBiconeOfIsSplitEpiOfKernel_pt, HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q, isIso_colimit_cocone_parallelPair_of_eq, CategoryTheory.regularTopology.parallelPair_pullback_initial, walkingParallelFamilyEquivWalkingParallelPair_inverse_map, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff, Fork.op_π, Cocone.ofCofork_ι, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id, Fork.app_one_eq_ι_comp_left, binaryBiconeOfIsSplitMonoOfCokernel_snd, preservesSplitEqualizers, cokernelBiproductιIso_inv, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair, kernelBiproductπIso_inv, cokernelBiproductFromSubtypeIso_hom, walkingParallelPairOpEquiv_unitIso_inv_app_zero, Fork.π_comp_hom_assoc, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_pt, CategoryTheory.ShortComplex.RightHomologyData.wι, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, CategoryTheory.Monad.beckCofork_pt, Fork.app_one_eq_ι_comp_right_assoc, CategoryTheory.Preadditive.mono_iff_isZero_kernel', binaryBiconeOfIsSplitMonoOfCokernel_inl, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_H, Cofork.condition, Cofork.app_zero_eq_comp_π_right, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, Multifork.toPiFork_π_app_one, Multifork.ofPiFork_pt, walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app, isIso_limit_cone_parallelPair_of_eq, reflexiveCoforkEquivCofork_functor_obj_π, coconeOfIsSplitEpi_pt, AddCommGrpCat.kernelIsoKer_inv_comp_ι, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, parallelPair_obj_one, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, parallelPair_functor_obj, SemiNormedGrp.hasLimit_parallelPair, SheafOfModules.Presentation.map_relations_I, CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app, id_tensor_π_preserves_coequalizer_inv_desc, reflexiveCoforkEquivCofork_inverse_obj_pt, Fork.condition, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc, CategoryTheory.ShortComplex.LeftHomologyData.wπ, walkingParallelPairOpEquiv_unitIso_inv_app_one, CategoryTheory.instHasLimitsOfShapeWalkingParallelPairInd, SheafOfModules.Presentation.mapRelations_mapGenerators, KernelFork.app_one, Fork.app_zero_eq_ι, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, parallelPairHom_app_one, isKernelCompMono_lift, SheafOfModules.relationsOfIsCokernelFree_I, CategoryTheory.IsSplitEqualizer.asFork_pt, MulticospanIndex.toPiForkFunctor_obj, Cofork.app_zero_eq_comp_π_right_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, Fork.equivOfIsos_inverse_obj_ι, CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.out, Cofork.IsColimit.homIso_natural, CokernelCofork.π_mapOfIsColimit_assoc, equalizerPullbackMapIso_hom_snd_assoc, Fork.op_ι_app, MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, CommRingCat.equalizer_ι_isLocalHom', CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.f, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, binaryBiconeOfIsSplitEpiOfKernel_snd, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, splitEpiOfIdempotentOfIsColimitCofork_section_, parallelPair_map_right, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, walkingParallelPairOp_zero, Fork.op_ι_app_one, mono_of_isLimit_fork, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app, MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, PreservesKernel.of_iso_comparison, CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv, equalizerPullbackMapIso_hom_snd, Cofork.unop_π_app_zero, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι_assoc, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι, Cofork.IsColimit.existsUnique, CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel, CokernelCofork.condition_assoc, parallelPair_initial_mk, equalizerPullbackMapIso_hom_fst, MultispanIndex.toSigmaCoforkFunctor_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, AlgebraicGeometry.isClosedImmersion_equalizer_ι_left, equalizerPullbackMapIso_inv_ι_snd_assoc, parallelPair_obj_zero, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, CategoryTheory.Monad.beckAlgebraCofork_ι_app, Cone.ofFork_π, MultispanIndex.parallelPairDiagramOfIsColimit_map, colimit_ι_zero_cokernel_desc, CokernelCofork.map_condition, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_K, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, preservesSplitCoequalizers, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, walkingParallelPairOpEquiv_unitIso_one, Fork.IsLimit.lift_ι_assoc, CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift, CategoryTheory.Preadditive.epi_iff_isZero_cokernel', CokernelCofork.map_π, Fork.IsLimit.lift_ι', CommRingCat.equalizer_ι_isLocalHom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, Multifork.ofPiFork_π_app_right, reflexiveCoforkEquivCofork_inverse_obj_π, cokernelBiprodInlIso_hom, Multifork.ofPiFork_π_app_left, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles, CategoryTheory.Subfunctor.equalizer.fork_pt, WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, binaryBiconeOfIsSplitEpiOfKernel_fst, walkingParallelPairOpEquiv_unitIso_zero, CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer', preservesEqualizers_of_preservesPullbacks_and_binaryProducts, CategoryTheory.Comonad.beckEqualizer_lift, MulticospanIndex.ofPiForkFunctor_obj, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_ι, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse, KernelFork.mapIsoOfIsLimit_hom, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_π, CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer', kernelBiprodSndIso_inv, CategoryTheory.Comonad.beckFork_pt, MulticospanIndex.parallelPairDiagramOfIsLimit_obj, CategoryTheory.NormalEpiCategory.hasColimit_parallelPair, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, KernelFork.map_condition, MultispanIndex.toSigmaCoforkFunctor_map_hom, SheafOfModules.relationsOfIsCokernelFree_s, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, Fork.op_ι_app_zero, Cofork.op_π_app_one, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, Cofork.IsColimit.π_desc, TopCat.isOpen_iff_of_isColimit_cofork, Bimod.whiskerRight_hom, TopCat.isQuotientMap_of_isColimit_cofork, KernelFork.map_ι, MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, equalizer.fork_π_app_zero, splitMonoOfIdempotentOfIsLimitFork_retraction, MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom_assoc, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, MulticospanIndex.ofPiForkFunctor_map_hom, WalkingParallelPair.inclusionWalkingReflexivePair_final, Cofork.ofπ_pt, parallelPair.eqOfHomEq_hom_app, CategoryTheory.ShortComplex.exact_iff_of_forks, coequalizer.cofork_ι_app_one, CategoryTheory.Functor.PreservesHomology.preservesCokernel, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff, coconeOfIsSplitEpi_ι_app, SheafOfModules.Presentation.IsFinite.finite_relations, walkingParallelPairOp_one, CategoryTheory.Monad.MonadicityInternal.counitCofork_pt, CokernelCofork.map_condition_assoc, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, walkingParallelFamilyEquivWalkingParallelPair_functor_obj, CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app, Multifork.ofPiFork_ι, Cofork.IsColimit.homIso_symm_apply, Fork.condition_assoc, Cofork.IsColimit.π_desc', CokernelCofork.π_eq_zero, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, isIso_colimit_cocone_parallelPair_of_self, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, Fork.isoForkOfι_inv_hom, Cofork.ofπ_ι_app, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom, walkingParallelPairOpEquiv_unitIso_hom_app_one, preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, Cofork.unop_ι, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_H, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_zero, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, WalkingParallelPair.instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, CokernelCofork.IsColimit.isZero_of_epi, opParallelPairIso_inv_app_zero, cokernelCoforkBiproductFromSubtype_cocone, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, opParallelPairIso_inv_app_one, walkingParallelPairOpEquiv_counitIso_one, HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, Multicofork.ofSigmaCofork_ι_app_left, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, coneOfIsSplitMono_pt, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι, parallelPair.eqOfHomEq_inv_app, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, equalizerPullbackMapIso_inv_ι_fst_assoc, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj, MultispanIndex.ofSigmaCoforkFunctor_map_hom, Cofork.IsColimit.π_desc'_assoc, CommRingCat.Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, cokernelBiproductFromSubtypeIso_inv, CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA, CategoryTheory.Comonad.beckCoalgebraFork_π_app, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, preservesCokernel_zero', CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app, preservesCokernel_zero, Types.equalizerIso_inv_comp_ι_apply, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom, diagramIsoParallelPair_inv_app, MultispanIndex.parallelPairDiagramOfIsColimit_obj, isIso_limit_cone_parallelPair_of_self, kernelForkBiproductToSubtype_isLimit, Cofork.app_one_eq_π, kernelBiproductToSubtypeIso_inv, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom, walkingParallelPairOpEquiv_counitIso_inv_app_op_one, HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app, CategoryTheory.parallel_pair_connected, walkingParallelPairOpEquiv_counitIso_hom_app_op_zero, Cofork.op_ι, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, walkingParallelPairOp_right, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor, CategoryTheory.Functor.PreservesHomology.preservesKernel, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f, AlgebraicGeometry.LocallyRingedSpace.preservesCoequalizer, Fork.unop_π, binaryBiconeOfIsSplitEpiOfKernel_inr, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair, coequalizer.π_colimMap_desc, Types.type_equalizer_iff_unique, isCokernelEpiComp_desc, isIso_limit_cocone_parallelPair_of_epi, MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom, CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out, KernelFork.mapOfIsLimit_ι, parallelPairHom_app_zero, walkingParallelPairOpEquiv_inverse, Fork.app_one_eq_ι_comp_right, CategoryTheory.Preadditive.coforkOfCokernelCofork_pt, binaryBiconeOfIsSplitMonoOfCokernel_fst, preservesKernel_zero', CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι, π_tensor_id_preserves_coequalizer_inv_colimMap_desc, FGModuleCat.instIsIsoCoimageImageComparison, epi_of_isColimit_cofork, KernelFork.map_condition_assoc, parallelPairOpIso_hom_app_zero
WalkingParallelPairHom 📖CompData—
coconeOfIsSplitEpi 📖CompOp
3 mathmath: coconeOfIsSplitEpi_pt, coconeOfIsSplitEpi_π, coconeOfIsSplitEpi_ι_app
coequalizer 📖CompOp
57 mathmath: coequalizer.π_of_self, Bimod.TensorBimod.π_tensor_id_actRight, map_π_preserves_coequalizer_inv_colimMap, Types.coequalizerIso_quot_comp_inv, Bimod.TensorBimod.whiskerLeft_π_actLeft, TopCat.coequalizer_isOpen_iff, Types.coequalizerIso_π_comp_hom_apply, map_π_preserves_coequalizer_inv_colimMap_desc, coequalizer.condition, coequalizer.π_epi, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, π_reflexiveCoequalizerIsoCoequalizer_inv_assoc, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, coequalizer.isoTargetOfSelf_inv, isPushout_coequalizer_coprod, Types.coequalizerIso_quot_comp_inv_apply, Types.coequalizerIso_π_comp_hom, CategoryTheory.Monad.MonadicityInternal.unitCofork_π, π_tensor_id_preserves_coequalizer_inv_desc, map_π_preserves_coequalizer_inv_colimMap_assoc, coequalizerComparison_map_desc, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, id_tensor_π_preserves_coequalizer_inv_desc, map_π_preserves_coequalizer_inv_assoc, ι_comp_coequalizerComparison_assoc, ι_colimitOfIsReflexivePairIsoCoequalizer_hom, PreservesCoequalizer.iso_hom, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, coequalizer.isoTargetOfSelf_hom, ι_comp_coequalizerComparison, π_colimitOfIsReflexivePairIsoCoequalizer_inv, coequalizer.π_desc_assoc, coequalizer.hom_ext_iff, π_reflexiveCoequalizerIsoCoequalizer_inv, ι_reflexiveCoequalizerIsoCoequalizer_hom, coequalizerComparison_map_desc_assoc, instIsIsoCoequalizerComparison, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, coequalizer.condition_assoc, map_π_preserves_coequalizer_inv_desc, coequalizer.existsUnique, π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, coequalizer.π_desc, ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, map_π_epi, map_π_preserves_coequalizer_inv, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc, coequalizer.π_of_eq, coequalizer.π_colimMap_desc, CategoryTheory.instIsRegularEpiπ, map_π_preserves_coequalizer_inv_desc_assoc, π_tensor_id_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Regular.instMonoDesc
coequalizerComparison 📖CompOp
6 mathmath: coequalizerComparison_map_desc, ι_comp_coequalizerComparison_assoc, PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison, coequalizerComparison_map_desc_assoc, instIsIsoCoequalizerComparison
coequalizerIsCoequalizer 📖CompOp—
coneOfIsSplitMono 📖CompOp
3 mathmath: coneOfIsSplitMono_ι, coneOfIsSplitMono_π_app, coneOfIsSplitMono_pt
diagramIsoParallelPair 📖CompOp
2 mathmath: diagramIsoParallelPair_hom_app, diagramIsoParallelPair_inv_app
equalizer 📖CompOp
48 mathmath: PreservesEqualizer.iso_hom, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, equalizer.ι_of_eq, equalizerComparison_comp_π, AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, equalizerSubobject_arrow'_assoc, equalizer.lift_ι, isPullback_equalizer_prod, AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated, AlgebraicGeometry.IsImmersion.instιScheme, CategoryTheory.instIsRegularMonoι, equalizerPullbackMapIso_inv_ι_snd, equalizerPullbackMapIso_inv_ι_fst, Types.equalizerIso_inv_comp_ι, equalizer.condition, equalizerPullbackMapIso_hom_fst_assoc, CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι, Types.equalizerIso_hom_comp_subtype_apply, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, instIsIsoEqualizerComparison, equalizer.lift_ι_assoc, Types.equalizerIso_hom_comp_subtype, equalizer.ι_mono, equalizer.condition_assoc, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, PreservesEqualizer.iso_inv_ι, equalizer.existsUnique, equalizerPullbackMapIso_hom_snd_assoc, equalizerSubobject_arrow, equalizerPullbackMapIso_hom_snd, equalizerPullbackMapIso_hom_fst, AlgebraicGeometry.isClosedImmersion_equalizer_ι_left, equalizerPullbackMapIso_inv_ι_snd_assoc, equalizerSubobject_arrow', equalizerSubobject_arrow_assoc, equalizer.ι_of_self, equalizer.isoSourceOfSelf_hom, equalizerComparison_comp_π_assoc, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, equalizerPullbackMapIso_inv_ι_fst_assoc, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux, map_lift_equalizerComparison_assoc, map_lift_equalizerComparison, Types.equalizerIso_inv_comp_ι_apply, equalizer.hom_ext_iff, equalizer.isoSourceOfSelf_inv, pullback_equalizer
equalizerComparison 📖CompOp
6 mathmath: PreservesEqualizer.iso_hom, equalizerComparison_comp_π, instIsIsoEqualizerComparison, equalizerComparison_comp_π_assoc, map_lift_equalizerComparison_assoc, map_lift_equalizerComparison
equalizerIsEqualizer 📖CompOp—
idCofork 📖CompOp—
idFork 📖CompOp—
instDecidableEqWalkingParallelPair 📖CompOp—
instDecidableEqWalkingParallelPairHom 📖CompOp—
instInhabitedWalkingParallelPair 📖CompOp—
instInhabitedWalkingParallelPairHomZeroOne 📖CompOp—
isCoequalizerEpiComp 📖CompOp—
isColimitIdCofork 📖CompOp—
isEqualizerCompMono 📖CompOp—
isLimitIdFork 📖CompOp—
isLimitPrecompFork 📖CompOp—
isSplitEpiCoequalizes 📖CompOp—
isSplitMonoEqualizes 📖CompOp—
liftPrecomp 📖CompOp—
parallelPair 📖CompOp
416 mathmath: Fork.IsLimit.homIso_natural, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc, cokernelBiproductιIso_hom, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition, MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom, HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt, AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg', Fork.IsLimit.lift_ι'_assoc, map_π_preserves_coequalizer_inv_colimMap, parallelPairOpIso_inv_app_zero, CategoryTheory.Comonad.ComonadicityInternal.unitFork_π_app, Types.coequalizerIso_quot_comp_inv, CategoryTheory.PreOneHypercover.forkOfIsColimit_pt, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg, kernelBiprodSndIso_hom, colimit_ι_zero_cokernel_desc_assoc, Fork.π_comp_hom, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, CategoryTheory.Comonad.beckCoalgebraFork_pt, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app, Bimod.whiskerLeft_hom, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, CategoryTheory.Comonad.ComonadicityInternal.unitFork_pt, CategoryTheory.Functor.PreservesHomology.preservesKernels, MulticospanIndex.multiforkEquivPiFork_functor_map_hom, walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app, Fork.unop_ι_app_zero, KernelFork.condition_assoc, KernelFork.mapOfIsLimit_ι_assoc, Cofork.ofCocone_ι, CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc, Fork.isoForkOfι_hom_hom, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, CategoryTheory.Monad.beckCoequalizer_desc, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc, Fork.IsLimit.mono, kernelForkBiproductToSubtype_cone, KernelFork.IsLimit.isZero_of_mono, CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, cokernelCoforkBiproductFromSubtype_isColimit, CategoryTheory.IsSplitCoequalizer.asCofork_pt, PreservesCokernel.of_iso_comparison, AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated, TopCat.coequalizer_isOpen_iff, kernelBiprodFstIso_hom, of_iso_comparison, AlgebraicGeometry.IsImmersion.instιScheme, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom, parallelPairOpIso_inv_app_one, Types.coequalizerIso_π_comp_hom_apply, kernelBiproductπIso_hom, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, Multicofork.ofSigmaCofork_ι_app_right', CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out, Fork.ofι_pt, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.f', equalizerPullbackMapIso_inv_ι_snd, CokernelCofork.π_mapOfIsColimit, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf', Cofork.unop_π_app_one, binaryBiconeOfIsSplitEpiOfKernel_inl, Cofork.IsColimit.epi, equalizerPullbackMapIso_inv_ι_fst, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, MulticospanIndex.toPiForkFunctor_map_hom, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, map_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, Types.equalizerIso_inv_comp_ι, PreservesEqualizer.of_iso_comparison, Cofork.condition_assoc, Fork.ι_postcompose, Fork.equivOfIsos_functor_obj_ι, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_H, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f, Fork.IsLimit.existsUnique, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, CokernelCofork.IsColimit.isIso_π, equalizerPullbackMapIso_hom_fst_assoc, Fork.hom_comp_ι, Multicofork.toSigmaCofork_pt, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, CategoryTheory.ShortComplex.RightHomologyData.wι_assoc, Multifork.toPiFork_pt, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, parallelPairOpIso_hom_app_one, preservesKernel_zero, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair, MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom, Fork.unop_ι_app_one, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι, CategoryTheory.NormalMonoCategory.hasLimit_parallelPair, kernelBiprodFstIso_inv, kernelBiproductToSubtypeIso_hom, CokernelCofork.condition, isIso_limit_cone_parallelPair_of_epi, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q, opParallelPairIso_hom_app_zero, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.g, binaryBiconeOfIsSplitMonoOfCokernel_inr, parallelPair_map_left, Fork.IsLimit.homIso_symm_apply, CategoryTheory.Monad.beckAlgebraCofork_pt, Cofork.app_zero_eq_comp_π_left, diagramIsoParallelPair_hom_app, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_H, CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer', cokernelBiprodInlIso_inv, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, opParallelPairIso_hom_app_one, Cofork.IsColimit.homIso_apply_coe, coneOfIsSplitMono_π_app, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf, CommRingCat.instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι, Multicofork.ofSigmaCofork_π, MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, CokernelCofork.mapIsoOfIsColimit_inv, Types.coequalizerIso_quot_comp_inv_apply, Multicofork.ofSigmaCofork_pt, CategoryTheory.Preadditive.forkOfKernelFork_pt, Fork.op_pt, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K, Types.coequalizerIso_π_comp_hom, Fork.ofι_π_app, Cofork.op_π_app_zero, Cofork.IsColimit.π_desc_assoc, MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.out, cokernelBiprodInrIso_inv, ωCPO.instHasLimitWalkingParallelPairParallelPair, MulticospanIndex.multiforkEquivPiFork_functor_obj_pt, walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app, Fork.hom_comp_ι_assoc, KernelFork.mapIsoOfIsLimit_inv, Types.equalizerIso_hom_comp_subtype_apply, MultispanIndex.ofSigmaCoforkFunctor_obj, CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair.out, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, binaryBiconeOfIsSplitMonoOfCokernel_pt, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt, CokernelCofork.mapIsoOfIsColimit_hom, Fork.ofCone_π, π_tensor_id_preserves_coequalizer_inv_desc, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair, KernelFork.IsLimit.isIso_ι, Cofork.π_precompose, CategoryTheory.Equalizer.Presieve.sheaf_condition, KernelFork.condition, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel, MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, Fork.IsLimit.homIso_apply_coe, map_π_preserves_coequalizer_inv_colimMap_assoc, Fork.IsLimit.lift_ι, Multicofork.ofSigmaCofork_ι_app_right, CategoryTheory.Functor.PreservesHomology.preservesCokernels, Types.equalizerIso_hom_comp_subtype, cokernelBiprodInrIso_hom, CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA, CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.g', binaryBiconeOfIsSplitEpiOfKernel_pt, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q, isIso_colimit_cocone_parallelPair_of_eq, CategoryTheory.regularTopology.parallelPair_pullback_initial, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff, Fork.op_π, Cocone.ofCofork_ι, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id, Fork.app_one_eq_ι_comp_left, binaryBiconeOfIsSplitMonoOfCokernel_snd, preservesSplitEqualizers, cokernelBiproductιIso_inv, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair, kernelBiproductπIso_inv, cokernelBiproductFromSubtypeIso_hom, Fork.π_comp_hom_assoc, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_pt, CategoryTheory.ShortComplex.RightHomologyData.wι, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, CategoryTheory.Monad.beckCofork_pt, Fork.app_one_eq_ι_comp_right_assoc, CategoryTheory.Preadditive.mono_iff_isZero_kernel', binaryBiconeOfIsSplitMonoOfCokernel_inl, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_H, Cofork.condition, Cofork.app_zero_eq_comp_π_right, Multifork.toPiFork_π_app_one, Multifork.ofPiFork_pt, walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app, isIso_limit_cone_parallelPair_of_eq, reflexiveCoforkEquivCofork_functor_obj_π, coconeOfIsSplitEpi_pt, AddCommGrpCat.kernelIsoKer_inv_comp_ι, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, parallelPair_obj_one, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, parallelPair_functor_obj, SemiNormedGrp.hasLimit_parallelPair, SheafOfModules.Presentation.map_relations_I, CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app, id_tensor_π_preserves_coequalizer_inv_desc, reflexiveCoforkEquivCofork_inverse_obj_pt, Fork.condition, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc, CategoryTheory.ShortComplex.LeftHomologyData.wπ, SheafOfModules.Presentation.mapRelations_mapGenerators, KernelFork.app_one, Fork.app_zero_eq_ι, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, parallelPairHom_app_one, isKernelCompMono_lift, SheafOfModules.relationsOfIsCokernelFree_I, CategoryTheory.IsSplitEqualizer.asFork_pt, MulticospanIndex.toPiForkFunctor_obj, Cofork.app_zero_eq_comp_π_right_assoc, Fork.equivOfIsos_inverse_obj_ι, CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.out, Cofork.IsColimit.homIso_natural, CokernelCofork.π_mapOfIsColimit_assoc, equalizerPullbackMapIso_hom_snd_assoc, Fork.op_ι_app, MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.f, binaryBiconeOfIsSplitEpiOfKernel_snd, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, splitEpiOfIdempotentOfIsColimitCofork_section_, parallelPair_map_right, Fork.op_ι_app_one, mono_of_isLimit_fork, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app, MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, PreservesKernel.of_iso_comparison, CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv, equalizerPullbackMapIso_hom_snd, Cofork.unop_π_app_zero, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι_assoc, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι, Cofork.IsColimit.existsUnique, CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel, CokernelCofork.condition_assoc, parallelPair_initial_mk, equalizerPullbackMapIso_hom_fst, MultispanIndex.toSigmaCoforkFunctor_obj, AlgebraicGeometry.isClosedImmersion_equalizer_ι_left, equalizerPullbackMapIso_inv_ι_snd_assoc, parallelPair_obj_zero, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, CategoryTheory.Monad.beckAlgebraCofork_ι_app, Cone.ofFork_π, colimit_ι_zero_cokernel_desc, CokernelCofork.map_condition, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_K, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, preservesSplitCoequalizers, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, Fork.IsLimit.lift_ι_assoc, CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift, CategoryTheory.Preadditive.epi_iff_isZero_cokernel', CokernelCofork.map_π, Fork.IsLimit.lift_ι', CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, Multifork.ofPiFork_π_app_right, reflexiveCoforkEquivCofork_inverse_obj_π, cokernelBiprodInlIso_hom, Multifork.ofPiFork_π_app_left, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles, CategoryTheory.Subfunctor.equalizer.fork_pt, binaryBiconeOfIsSplitEpiOfKernel_fst, CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer', CategoryTheory.Comonad.beckEqualizer_lift, MulticospanIndex.ofPiForkFunctor_obj, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_ι, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse, KernelFork.mapIsoOfIsLimit_hom, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_π, CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer', kernelBiprodSndIso_inv, CategoryTheory.Comonad.beckFork_pt, CategoryTheory.NormalEpiCategory.hasColimit_parallelPair, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, KernelFork.map_condition, MultispanIndex.toSigmaCoforkFunctor_map_hom, SheafOfModules.relationsOfIsCokernelFree_s, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, Fork.op_ι_app_zero, Cofork.op_π_app_one, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, Cofork.IsColimit.π_desc, TopCat.isOpen_iff_of_isColimit_cofork, Bimod.whiskerRight_hom, TopCat.isQuotientMap_of_isColimit_cofork, KernelFork.map_ι, MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, equalizer.fork_π_app_zero, splitMonoOfIdempotentOfIsLimitFork_retraction, MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom_assoc, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, MulticospanIndex.ofPiForkFunctor_map_hom, Cofork.ofπ_pt, parallelPair.eqOfHomEq_hom_app, CategoryTheory.ShortComplex.exact_iff_of_forks, coequalizer.cofork_ι_app_one, CategoryTheory.Functor.PreservesHomology.preservesCokernel, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff, coconeOfIsSplitEpi_ι_app, SheafOfModules.Presentation.IsFinite.finite_relations, CategoryTheory.Monad.MonadicityInternal.counitCofork_pt, CokernelCofork.map_condition_assoc, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app, Multifork.ofPiFork_ι, Cofork.IsColimit.homIso_symm_apply, Fork.condition_assoc, Cofork.IsColimit.π_desc', CokernelCofork.π_eq_zero, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, isIso_colimit_cocone_parallelPair_of_self, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, Fork.isoForkOfι_inv_hom, Cofork.ofπ_ι_app, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, Cofork.unop_ι, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_H, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_zero, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, CokernelCofork.IsColimit.isZero_of_epi, opParallelPairIso_inv_app_zero, cokernelCoforkBiproductFromSubtype_cocone, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, opParallelPairIso_inv_app_one, HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app, Multicofork.ofSigmaCofork_ι_app_left, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, coneOfIsSplitMono_pt, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app, MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι, parallelPair.eqOfHomEq_inv_app, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, equalizerPullbackMapIso_inv_ι_fst_assoc, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj, MultispanIndex.ofSigmaCoforkFunctor_map_hom, Cofork.IsColimit.π_desc'_assoc, CommRingCat.Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, cokernelBiproductFromSubtypeIso_inv, CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA, CategoryTheory.Comonad.beckCoalgebraFork_π_app, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, preservesCokernel_zero', CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app, preservesCokernel_zero, Types.equalizerIso_inv_comp_ι_apply, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom, diagramIsoParallelPair_inv_app, isIso_limit_cone_parallelPair_of_self, kernelForkBiproductToSubtype_isLimit, Cofork.app_one_eq_π, kernelBiproductToSubtypeIso_inv, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom, HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app, Cofork.op_ι, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor, CategoryTheory.Functor.PreservesHomology.preservesKernel, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f, Fork.unop_π, binaryBiconeOfIsSplitEpiOfKernel_inr, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair, coequalizer.π_colimMap_desc, Types.type_equalizer_iff_unique, isCokernelEpiComp_desc, isIso_limit_cocone_parallelPair_of_epi, MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom, CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out, KernelFork.mapOfIsLimit_ι, parallelPairHom_app_zero, Fork.app_one_eq_ι_comp_right, CategoryTheory.Preadditive.coforkOfCokernelCofork_pt, binaryBiconeOfIsSplitMonoOfCokernel_fst, preservesKernel_zero', CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι, π_tensor_id_preserves_coequalizer_inv_colimMap_desc, epi_of_isColimit_cofork, KernelFork.map_condition_assoc, parallelPairOpIso_hom_app_zero
parallelPairHom 📖CompOp
11 mathmath: map_π_preserves_coequalizer_inv_colimMap, Bimod.whiskerLeft_hom, map_π_preserves_coequalizer_inv_colimMap_desc, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, map_π_preserves_coequalizer_inv_colimMap_assoc, parallelPairHom_app_one, Bimod.whiskerRight_hom, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, coequalizer.π_colimMap_desc, parallelPairHom_app_zero, π_tensor_id_preserves_coequalizer_inv_colimMap_desc
parallelPairHomMk 📖CompOp
1 mathmath: parallelPairHomMk_app
parallelPairIso 📖CompOp—
parallelPairIsoMk 📖CompOp
3 mathmath: parallelPairIsoMk_inv_app, parallelPairIsoMk_hom_app, SheafOfModules.Presentation.map_relations_I
precompFork 📖CompOp—
splitEpiOfCoequalizer 📖CompOp—
splitEpiOfIdempotentCoequalizer 📖CompOp—
splitEpiOfIdempotentOfIsColimitCofork 📖CompOp
1 mathmath: splitEpiOfIdempotentOfIsColimitCofork_section_
splitMonoOfEqualizer 📖CompOp—
splitMonoOfIdempotentEqualizer 📖CompOp—
splitMonoOfIdempotentOfIsLimitFork 📖CompOp
1 mathmath: splitMonoOfIdempotentOfIsLimitFork_retraction
walkingParallelPairHomCategory 📖CompOp
484 mathmath: Fork.IsLimit.homIso_natural, walkingParallelPairOpEquiv_unitIso_hom_app_zero, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc, cokernelBiproductιIso_hom, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition, MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt, AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg', Fork.IsLimit.lift_ι'_assoc, walkingParallelPairOp_left, map_π_preserves_coequalizer_inv_colimMap, parallelPairOpIso_inv_app_zero, CategoryTheory.Comonad.ComonadicityInternal.unitFork_π_app, Types.coequalizerIso_quot_comp_inv, CategoryTheory.PreOneHypercover.forkOfIsColimit_pt, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg, kernelBiprodSndIso_hom, colimit_ι_zero_cokernel_desc_assoc, Fork.π_comp_hom, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, CategoryTheory.Comonad.beckCoalgebraFork_pt, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app, Bimod.whiskerLeft_hom, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, CategoryTheory.Comonad.ComonadicityInternal.unitFork_pt, CategoryTheory.Functor.PreservesHomology.preservesKernels, MulticospanIndex.multiforkEquivPiFork_functor_map_hom, walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app, walkingParallelPairOpEquiv_counitIso_hom_app_op_one, Fork.unop_ι_app_zero, isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair, KernelFork.condition_assoc, KernelFork.mapOfIsLimit_ι_assoc, Cofork.ofCocone_ι, walkingParallelPairOpEquiv_counitIso_inv_app_op_zero, CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc, Fork.isoForkOfι_hom_hom, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, CategoryTheory.Monad.beckCoequalizer_desc, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc, Fork.IsLimit.mono, kernelForkBiproductToSubtype_cone, KernelFork.IsLimit.isZero_of_mono, CategoryTheory.Monad.ReflectsColimitOfIsSplitPair.out, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, cokernelCoforkBiproductFromSubtype_isColimit, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, CategoryTheory.IsSplitCoequalizer.asCofork_pt, PreservesCokernel.of_iso_comparison, AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated, TopCat.coequalizer_isOpen_iff, kernelBiprodFstIso_hom, walkingParallelPairHom_id, of_iso_comparison, AlgebraicGeometry.IsImmersion.instιScheme, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom, closedUnderLimitsOfShape_walkingParallelPair_isIndObject, WalkingParallelPair.inclusionWalkingReflexivePair_map, parallelPairOpIso_inv_app_one, Types.coequalizerIso_π_comp_hom_apply, MulticospanIndex.parallelPairDiagram_map, kernelBiproductπIso_hom, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, Multicofork.ofSigmaCofork_ι_app_right', CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out, Fork.ofι_pt, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.f', equalizerPullbackMapIso_inv_ι_snd, CokernelCofork.π_mapOfIsColimit, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf', Cofork.unop_π_app_one, binaryBiconeOfIsSplitEpiOfKernel_inl, Cofork.IsColimit.epi, CategoryTheory.instHasColimitsOfShapeWalkingParallelPairInd, walkingParallelPairOpEquiv_counitIso_zero, equalizerPullbackMapIso_inv_ι_fst, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, MulticospanIndex.toPiForkFunctor_map_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, map_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, Types.equalizerIso_inv_comp_ι, PreservesEqualizer.of_iso_comparison, Cofork.condition_assoc, Fork.ι_postcompose, Fork.equivOfIsos_functor_obj_ι, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_H, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f, Fork.IsLimit.existsUnique, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, CokernelCofork.IsColimit.isIso_π, equalizerPullbackMapIso_hom_fst_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, Fork.hom_comp_ι, Multicofork.toSigmaCofork_pt, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, CategoryTheory.ShortComplex.RightHomologyData.wι_assoc, Multifork.toPiFork_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, parallelPairOpIso_hom_app_one, preservesKernel_zero, HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair, MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom, Fork.unop_ι_app_one, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι, CategoryTheory.NormalMonoCategory.hasLimit_parallelPair, kernelBiprodFstIso_inv, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, kernelBiproductToSubtypeIso_hom, CokernelCofork.condition, isIso_limit_cone_parallelPair_of_epi, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q, opParallelPairIso_hom_app_zero, CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.g, binaryBiconeOfIsSplitMonoOfCokernel_inr, parallelPair_map_left, Fork.IsLimit.homIso_symm_apply, CategoryTheory.Monad.beckAlgebraCofork_pt, Cofork.app_zero_eq_comp_π_left, diagramIsoParallelPair_hom_app, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_H, CommRingCat.Under.instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier, CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer', cokernelBiprodInlIso_inv, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, opParallelPairIso_hom_app_one, Cofork.IsColimit.homIso_apply_coe, coneOfIsSplitMono_π_app, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf, MulticospanIndex.parallelPairDiagram_obj, CommRingCat.instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι, Multicofork.ofSigmaCofork_π, MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, CokernelCofork.mapIsoOfIsColimit_inv, Types.coequalizerIso_quot_comp_inv_apply, Multicofork.ofSigmaCofork_pt, CategoryTheory.Preadditive.forkOfKernelFork_pt, Fork.op_pt, walkingParallelPairOpEquiv_functor, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K, Types.coequalizerIso_π_comp_hom, Fork.ofι_π_app, Cofork.op_π_app_zero, Cofork.IsColimit.π_desc_assoc, MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.out, cokernelBiprodInrIso_inv, ωCPO.instHasLimitWalkingParallelPairParallelPair, MulticospanIndex.multiforkEquivPiFork_functor_obj_pt, walkingParallelFamilyEquivWalkingParallelPair_functor_map, walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app, Fork.hom_comp_ι_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, walkingParallelFamilyEquivWalkingParallelPair_inverse_obj, KernelFork.mapIsoOfIsLimit_inv, Types.equalizerIso_hom_comp_subtype_apply, WalkingParallelPair.inclusionWalkingReflexivePair_obj, MultispanIndex.ofSigmaCoforkFunctor_obj, CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair.out, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, binaryBiconeOfIsSplitMonoOfCokernel_pt, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt, CokernelCofork.mapIsoOfIsColimit_hom, Fork.ofCone_π, π_tensor_id_preserves_coequalizer_inv_desc, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair, KernelFork.IsLimit.isIso_ι, Cofork.π_precompose, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, CategoryTheory.Equalizer.Presieve.sheaf_condition, KernelFork.condition, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel, MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, MulticospanIndex.parallelPairDiagramOfIsLimit_map, Fork.IsLimit.homIso_apply_coe, map_π_preserves_coequalizer_inv_colimMap_assoc, Fork.IsLimit.lift_ι, Multicofork.ofSigmaCofork_ι_app_right, CategoryTheory.Functor.PreservesHomology.preservesCokernels, Types.equalizerIso_hom_comp_subtype, cokernelBiprodInrIso_hom, CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA, CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc, CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.g', binaryBiconeOfIsSplitEpiOfKernel_pt, HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q, isIso_colimit_cocone_parallelPair_of_eq, CategoryTheory.regularTopology.parallelPair_pullback_initial, walkingParallelFamilyEquivWalkingParallelPair_inverse_map, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff, Fork.op_π, Cocone.ofCofork_ι, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id, Fork.app_one_eq_ι_comp_left, binaryBiconeOfIsSplitMonoOfCokernel_snd, preservesSplitEqualizers, cokernelBiproductιIso_inv, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair, kernelBiproductπIso_inv, cokernelBiproductFromSubtypeIso_hom, walkingParallelPairOpEquiv_unitIso_inv_app_zero, Fork.π_comp_hom_assoc, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt, reflexiveCoforkEquivCofork_functor_obj_pt, CategoryTheory.ShortComplex.RightHomologyData.wι, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, CategoryTheory.Monad.beckCofork_pt, Fork.app_one_eq_ι_comp_right_assoc, CategoryTheory.Preadditive.mono_iff_isZero_kernel', binaryBiconeOfIsSplitMonoOfCokernel_inl, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_H, Cofork.condition, Cofork.app_zero_eq_comp_π_right, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, Multifork.toPiFork_π_app_one, Multifork.ofPiFork_pt, walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app, isIso_limit_cone_parallelPair_of_eq, reflexiveCoforkEquivCofork_functor_obj_π, coconeOfIsSplitEpi_pt, AddCommGrpCat.kernelIsoKer_inv_comp_ι, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, parallelPair_obj_one, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, parallelPair_functor_obj, SemiNormedGrp.hasLimit_parallelPair, SheafOfModules.Presentation.map_relations_I, CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app, id_tensor_π_preserves_coequalizer_inv_desc, reflexiveCoforkEquivCofork_inverse_obj_pt, Fork.condition, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc, CategoryTheory.ShortComplex.LeftHomologyData.wπ, walkingParallelPairOpEquiv_unitIso_inv_app_one, CategoryTheory.instHasLimitsOfShapeWalkingParallelPairInd, SheafOfModules.Presentation.mapRelations_mapGenerators, KernelFork.app_one, Fork.app_zero_eq_ι, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, parallelPairHom_app_one, isKernelCompMono_lift, SheafOfModules.relationsOfIsCokernelFree_I, CategoryTheory.IsSplitEqualizer.asFork_pt, MulticospanIndex.toPiForkFunctor_obj, Cofork.app_zero_eq_comp_π_right_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, Fork.equivOfIsos_inverse_obj_ι, CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.out, Cofork.IsColimit.homIso_natural, CokernelCofork.π_mapOfIsColimit_assoc, equalizerPullbackMapIso_hom_snd_assoc, Fork.op_ι_app, MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, CommRingCat.equalizer_ι_isLocalHom', CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.f, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, binaryBiconeOfIsSplitEpiOfKernel_snd, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, splitEpiOfIdempotentOfIsColimitCofork_section_, parallelPair_map_right, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, walkingParallelPairOp_zero, Fork.op_ι_app_one, mono_of_isLimit_fork, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app, MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, PreservesKernel.of_iso_comparison, CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv, equalizerPullbackMapIso_hom_snd, Cofork.unop_π_app_zero, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι_assoc, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι, Cofork.IsColimit.existsUnique, CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel, CokernelCofork.condition_assoc, parallelPair_initial_mk, equalizerPullbackMapIso_hom_fst, MultispanIndex.toSigmaCoforkFunctor_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, AlgebraicGeometry.isClosedImmersion_equalizer_ι_left, equalizerPullbackMapIso_inv_ι_snd_assoc, parallelPair_obj_zero, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, CategoryTheory.Monad.beckAlgebraCofork_ι_app, Cone.ofFork_π, MultispanIndex.parallelPairDiagramOfIsColimit_map, colimit_ι_zero_cokernel_desc, CokernelCofork.map_condition, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_K, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, preservesSplitCoequalizers, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, walkingParallelPairOpEquiv_unitIso_one, Fork.IsLimit.lift_ι_assoc, CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift, CategoryTheory.Preadditive.epi_iff_isZero_cokernel', CokernelCofork.map_π, Fork.IsLimit.lift_ι', CommRingCat.equalizer_ι_isLocalHom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, Multifork.ofPiFork_π_app_right, reflexiveCoforkEquivCofork_inverse_obj_π, cokernelBiprodInlIso_hom, Multifork.ofPiFork_π_app_left, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles, CategoryTheory.Subfunctor.equalizer.fork_pt, WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, binaryBiconeOfIsSplitEpiOfKernel_fst, walkingParallelPairOpEquiv_unitIso_zero, CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer', preservesEqualizers_of_preservesPullbacks_and_binaryProducts, CategoryTheory.Comonad.beckEqualizer_lift, MulticospanIndex.ofPiForkFunctor_obj, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_ι, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse, KernelFork.mapIsoOfIsLimit_hom, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_π, CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer', kernelBiprodSndIso_inv, CategoryTheory.Comonad.beckFork_pt, MulticospanIndex.parallelPairDiagramOfIsLimit_obj, CategoryTheory.NormalEpiCategory.hasColimit_parallelPair, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, KernelFork.map_condition, MultispanIndex.toSigmaCoforkFunctor_map_hom, SheafOfModules.relationsOfIsCokernelFree_s, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, Fork.op_ι_app_zero, Cofork.op_π_app_one, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, Cofork.IsColimit.π_desc, TopCat.isOpen_iff_of_isColimit_cofork, Bimod.whiskerRight_hom, TopCat.isQuotientMap_of_isColimit_cofork, KernelFork.map_ι, MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, equalizer.fork_π_app_zero, splitMonoOfIdempotentOfIsLimitFork_retraction, MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom_assoc, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, MulticospanIndex.ofPiForkFunctor_map_hom, WalkingParallelPair.inclusionWalkingReflexivePair_final, Cofork.ofπ_pt, parallelPair.eqOfHomEq_hom_app, CategoryTheory.ShortComplex.exact_iff_of_forks, coequalizer.cofork_ι_app_one, CategoryTheory.Functor.PreservesHomology.preservesCokernel, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff, coconeOfIsSplitEpi_ι_app, SheafOfModules.Presentation.IsFinite.finite_relations, walkingParallelPairOp_one, CategoryTheory.Monad.MonadicityInternal.counitCofork_pt, CokernelCofork.map_condition_assoc, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, walkingParallelFamilyEquivWalkingParallelPair_functor_obj, CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app, Multifork.ofPiFork_ι, Cofork.IsColimit.homIso_symm_apply, Fork.condition_assoc, Cofork.IsColimit.π_desc', CokernelCofork.π_eq_zero, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, isIso_colimit_cocone_parallelPair_of_self, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, Fork.isoForkOfι_inv_hom, Cofork.ofπ_ι_app, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom, walkingParallelPairOpEquiv_unitIso_hom_app_one, preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, Cofork.unop_ι, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_H, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_zero, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, WalkingParallelPair.instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, CokernelCofork.IsColimit.isZero_of_epi, opParallelPairIso_inv_app_zero, cokernelCoforkBiproductFromSubtype_cocone, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, opParallelPairIso_inv_app_one, walkingParallelPairOpEquiv_counitIso_one, HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, Multicofork.ofSigmaCofork_ι_app_left, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, coneOfIsSplitMono_pt, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι, parallelPair.eqOfHomEq_inv_app, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, equalizerPullbackMapIso_inv_ι_fst_assoc, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj, MultispanIndex.ofSigmaCoforkFunctor_map_hom, Cofork.IsColimit.π_desc'_assoc, CommRingCat.Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, cokernelBiproductFromSubtypeIso_inv, CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA, CategoryTheory.Comonad.beckCoalgebraFork_π_app, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, preservesCokernel_zero', CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app, preservesCokernel_zero, Types.equalizerIso_inv_comp_ι_apply, MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom, diagramIsoParallelPair_inv_app, MultispanIndex.parallelPairDiagramOfIsColimit_obj, isIso_limit_cone_parallelPair_of_self, kernelForkBiproductToSubtype_isLimit, Cofork.app_one_eq_π, kernelBiproductToSubtypeIso_inv, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom, walkingParallelPairOpEquiv_counitIso_inv_app_op_one, HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app, CategoryTheory.parallel_pair_connected, walkingParallelPairOpEquiv_counitIso_hom_app_op_zero, Cofork.op_ι, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, walkingParallelPairOp_right, MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor, CategoryTheory.Functor.PreservesHomology.preservesKernel, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f, AlgebraicGeometry.LocallyRingedSpace.preservesCoequalizer, Fork.unop_π, binaryBiconeOfIsSplitEpiOfKernel_inr, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair, coequalizer.π_colimMap_desc, Types.type_equalizer_iff_unique, isCokernelEpiComp_desc, isIso_limit_cocone_parallelPair_of_epi, MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom, CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out, KernelFork.mapOfIsLimit_ι, parallelPairHom_app_zero, walkingParallelPairOpEquiv_inverse, Fork.app_one_eq_ι_comp_right, CategoryTheory.Preadditive.coforkOfCokernelCofork_pt, binaryBiconeOfIsSplitMonoOfCokernel_fst, preservesKernel_zero', CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι, π_tensor_id_preserves_coequalizer_inv_colimMap_desc, FGModuleCat.instIsIsoCoimageImageComparison, epi_of_isColimit_cofork, KernelFork.map_condition_assoc, parallelPairOpIso_hom_app_zero
walkingParallelPairOp 📖CompOp
7 mathmath: walkingParallelPairOp_left, walkingParallelPairOpEquiv_functor, Fork.op_ι_app, walkingParallelPairOp_zero, walkingParallelPairOp_one, walkingParallelPairOp_right, walkingParallelPairOpEquiv_inverse
walkingParallelPairOpEquiv 📖CompOp
23 mathmath: walkingParallelPairOpEquiv_unitIso_hom_app_zero, parallelPairOpIso_inv_app_zero, walkingParallelPairOpEquiv_counitIso_hom_app_op_one, walkingParallelPairOpEquiv_counitIso_inv_app_op_zero, parallelPairOpIso_inv_app_one, walkingParallelPairOpEquiv_counitIso_zero, parallelPairOpIso_hom_app_one, opParallelPairIso_hom_app_zero, opParallelPairIso_hom_app_one, walkingParallelPairOpEquiv_functor, walkingParallelPairOpEquiv_unitIso_inv_app_zero, walkingParallelPairOpEquiv_unitIso_inv_app_one, Fork.op_ι_app, walkingParallelPairOpEquiv_unitIso_one, walkingParallelPairOpEquiv_unitIso_zero, walkingParallelPairOpEquiv_unitIso_hom_app_one, opParallelPairIso_inv_app_zero, opParallelPairIso_inv_app_one, walkingParallelPairOpEquiv_counitIso_one, walkingParallelPairOpEquiv_counitIso_inv_app_op_one, walkingParallelPairOpEquiv_counitIso_hom_app_op_zero, walkingParallelPairOpEquiv_inverse, parallelPairOpIso_hom_app_zero

Theorems

NameKindAssumesProvesValidatesDepends On
coconeOfIsSplitEpi_pt 📖mathematical—Cocone.pt
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.section_
coconeOfIsSplitEpi		——
coconeOfIsSplitEpi_ι_app 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.section_
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cocone.ι
coconeOfIsSplitEpi
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
WalkingParallelPair.zero		——
coconeOfIsSplitEpi_π 📖mathematical—Cofork.π
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.section_
coconeOfIsSplitEpi		——
coequalizerComparison_map_desc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		coequalizer
CategoryTheory.Functor.obj
CategoryTheory.Functor.map
coequalizerComparison
coequalizer.desc		—coequalizer.hom_ext
ι_comp_coequalizerComparison_assoc
CategoryTheory.Functor.map_comp
colimit.ι_desc
coequalizerComparison_map_desc_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		coequalizer
CategoryTheory.Functor.obj
CategoryTheory.Functor.map
coequalizerComparison
coequalizer.desc		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
coequalizerComparison_map_desc
coneOfIsSplitMono_pt 📖mathematical—Cone.pt
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.retraction
coneOfIsSplitMono		——
coneOfIsSplitMono_ι 📖mathematical—Fork.ι
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.retraction
coneOfIsSplitMono		——
coneOfIsSplitMono_π_app 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
parallelPair
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.retraction
Cone.π
coneOfIsSplitMono
WalkingParallelPair.zero
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
WalkingParallelPair.one		——
diagramIsoParallelPair_hom_app 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
CategoryTheory.Functor.obj
WalkingParallelPair.zero
WalkingParallelPair.one
CategoryTheory.Functor.map
WalkingParallelPairHom.left
WalkingParallelPairHom.right
CategoryTheory.Iso.hom
CategoryTheory.Functor
CategoryTheory.Functor.category
diagramIsoParallelPair
CategoryTheory.eqToHom
CategoryTheory.Category.toCategoryStruct		——
diagramIsoParallelPair_inv_app 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
CategoryTheory.Functor.obj
WalkingParallelPair.zero
WalkingParallelPair.one
CategoryTheory.Functor.map
WalkingParallelPairHom.left
WalkingParallelPairHom.right
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
diagramIsoParallelPair
CategoryTheory.eqToHom
CategoryTheory.Category.toCategoryStruct		——
epi_of_isColimit_cofork 📖mathematical—CategoryTheory.Epi
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cocone.pt
Cofork.π		—Cofork.IsColimit.hom_ext
eq_of_epi_equalizer 📖————CategoryTheory.cancel_epi
equalizer.condition
eq_of_epi_fork_ι 📖————CategoryTheory.cancel_epi
Fork.condition
eq_of_mono_coequalizer 📖————CategoryTheory.cancel_mono
coequalizer.condition
eq_of_mono_cofork_π 📖————CategoryTheory.cancel_mono
Cofork.condition
equalizerComparison_comp_π 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
equalizer
CategoryTheory.Functor.map
equalizerComparison
equalizer.ι		—equalizer.lift_ι
equalizerComparison_comp_π_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
equalizer
CategoryTheory.Functor.map
equalizerComparison
equalizer.ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
equalizerComparison_comp_π
hasCoequalizer_epi_comp 📖mathematical—HasCoequalizer
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		——
hasCoequalizer_of_self 📖mathematical—HasCoequalizer——
hasCoequalizers_of_hasColimit_parallelPair 📖mathematicalHasColimit
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair		HasCoequalizers—hasColimit_of_iso
hasEqualizer_comp_mono 📖mathematical—HasEqualizer
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		——
hasEqualizer_of_self 📖mathematical—HasEqualizer——
hasEqualizer_precomp_of_equalizer 📖mathematical—HasEqualizer
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		——
hasEqualizer_precomp_of_hasEqualizer 📖mathematical—HasEqualizer
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		—hasEqualizer_precomp_of_equalizer
equalizer.condition
hasEqualizers_of_hasLimit_parallelPair 📖mathematicalHasLimit
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair		HasEqualizers—hasLimit_of_iso
isIso_colimit_cocone_parallelPair_of_eq 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cocone.pt
Cofork.π		—CategoryTheory.Iso.isIso_hom
isIso_colimit_cocone_parallelPair_of_self 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cocone.pt
Cofork.π		—isIso_colimit_cocone_parallelPair_of_eq
isIso_limit_cocone_parallelPair_of_epi 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cocone.pt
Cofork.π		—isIso_colimit_cocone_parallelPair_of_eq
CategoryTheory.cancel_mono
Cofork.condition
isIso_limit_cone_parallelPair_of_epi 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cone.pt
parallelPair
WalkingParallelPair.zero
Fork.ι		—isIso_limit_cone_parallelPair_of_eq
CategoryTheory.cancel_epi
Fork.condition
isIso_limit_cone_parallelPair_of_eq 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cone.pt
parallelPair
WalkingParallelPair.zero
Fork.ι		—CategoryTheory.Iso.isIso_hom
isIso_limit_cone_parallelPair_of_self 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cone.pt
parallelPair
WalkingParallelPair.zero
Fork.ι		—isIso_limit_cone_parallelPair_of_eq
map_lift_equalizerComparison 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Functor.obj
equalizer
CategoryTheory.Functor.map
equalizer.lift
equalizerComparison		—equalizer.hom_ext
CategoryTheory.Category.assoc
equalizerComparison_comp_π
CategoryTheory.Functor.map_comp
limit.lift_π
map_lift_equalizerComparison_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Functor.obj
equalizer
CategoryTheory.Functor.map
equalizer.lift
equalizerComparison		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
map_lift_equalizerComparison
mono_of_isLimit_fork 📖mathematical—CategoryTheory.Mono
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cone.pt
parallelPair
WalkingParallelPair.zero
Fork.ι		—Fork.IsLimit.hom_ext
parallelPairHomMk_app 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
WalkingParallelPair.zero
WalkingParallelPair.one
CategoryTheory.CategoryStruct.comp
CategoryTheory.Functor.map
WalkingParallelPairHom.left
WalkingParallelPairHom.right		CategoryTheory.NatTrans.app
parallelPairHomMk		——
parallelPairHom_app_one 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
parallelPairHom
WalkingParallelPair.one		——
parallelPairHom_app_zero 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
parallelPairHom
WalkingParallelPair.zero		——
parallelPairIsoMk_hom_app 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
WalkingParallelPair.zero
WalkingParallelPair.one
CategoryTheory.CategoryStruct.comp
CategoryTheory.Functor.map
WalkingParallelPairHom.left
CategoryTheory.Iso.hom
WalkingParallelPairHom.right		CategoryTheory.NatTrans.app
CategoryTheory.Functor
CategoryTheory.Functor.category
parallelPairIsoMk
CategoryTheory.Iso		——
parallelPairIsoMk_inv_app 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
WalkingParallelPair.zero
WalkingParallelPair.one
CategoryTheory.CategoryStruct.comp
CategoryTheory.Functor.map
WalkingParallelPairHom.left
CategoryTheory.Iso.hom
WalkingParallelPairHom.right		CategoryTheory.NatTrans.app
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
parallelPairIsoMk
CategoryTheory.Iso		——
parallelPair_functor_obj 📖mathematical—CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.zero
WalkingParallelPair.one
CategoryTheory.Functor.map
WalkingParallelPairHom.left
WalkingParallelPairHom.right		——
parallelPair_map_left 📖mathematical—CategoryTheory.Functor.map
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.zero
WalkingParallelPair.one
WalkingParallelPairHom.left		——
parallelPair_map_right 📖mathematical—CategoryTheory.Functor.map
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.zero
WalkingParallelPair.one
WalkingParallelPairHom.right		——
parallelPair_obj_one 📖mathematical—CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.one		——
parallelPair_obj_zero 📖mathematical—CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
WalkingParallelPair.zero		——
splitEpiOfIdempotentOfIsColimitCofork_section_ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.SplitEpi.section_
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
parallelPair
CategoryTheory.CategoryStruct.id
WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cocone.pt
Cofork.π
splitEpiOfIdempotentOfIsColimitCofork
IsColimit.desc
Cofork.ofπ		——
splitMonoOfIdempotentOfIsLimitFork_retraction 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.SplitMono.retraction
CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
Cone.pt
parallelPair
CategoryTheory.CategoryStruct.id
WalkingParallelPair.zero
Fork.ι
splitMonoOfIdempotentOfIsLimitFork
IsLimit.lift
Fork.ofι		——
walkingParallelPairHom_id 📖mathematical—WalkingParallelPairHom.id
CategoryTheory.CategoryStruct.id
WalkingParallelPair
CategoryTheory.Category.toCategoryStruct
walkingParallelPairHomCategory		——
walkingParallelPairOpEquiv_counitIso_hom_app_op_one 📖mathematical—CategoryTheory.NatTrans.app
Opposite
WalkingParallelPair
CategoryTheory.Category.opposite
walkingParallelPairHomCategory
CategoryTheory.Functor.comp
CategoryTheory.Equivalence.inverse
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.functor
CategoryTheory.Functor.id
CategoryTheory.Iso.hom
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.counitIso
Opposite.op
WalkingParallelPair.one
CategoryTheory.CategoryStruct.id
CategoryTheory.CategoryStruct.opposite
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_counitIso_hom_app_op_zero 📖mathematical—CategoryTheory.NatTrans.app
Opposite
WalkingParallelPair
CategoryTheory.Category.opposite
walkingParallelPairHomCategory
CategoryTheory.Functor.comp
CategoryTheory.Equivalence.inverse
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.functor
CategoryTheory.Functor.id
CategoryTheory.Iso.hom
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.counitIso
Opposite.op
WalkingParallelPair.zero
CategoryTheory.CategoryStruct.id
CategoryTheory.CategoryStruct.opposite
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_counitIso_inv_app_op_one 📖mathematical—CategoryTheory.NatTrans.app
Opposite
WalkingParallelPair
CategoryTheory.Category.opposite
walkingParallelPairHomCategory
CategoryTheory.Functor.id
CategoryTheory.Functor.comp
CategoryTheory.Equivalence.inverse
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.functor
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.counitIso
Opposite.op
WalkingParallelPair.one
CategoryTheory.CategoryStruct.id
CategoryTheory.CategoryStruct.opposite
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_counitIso_inv_app_op_zero 📖mathematical—CategoryTheory.NatTrans.app
Opposite
WalkingParallelPair
CategoryTheory.Category.opposite
walkingParallelPairHomCategory
CategoryTheory.Functor.id
CategoryTheory.Functor.comp
CategoryTheory.Equivalence.inverse
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.functor
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.counitIso
Opposite.op
WalkingParallelPair.zero
CategoryTheory.CategoryStruct.id
CategoryTheory.CategoryStruct.opposite
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_counitIso_one 📖mathematical—CategoryTheory.Iso.app
Opposite
WalkingParallelPair
CategoryTheory.Category.opposite
walkingParallelPairHomCategory
CategoryTheory.Functor.comp
CategoryTheory.Equivalence.inverse
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.functor
CategoryTheory.Functor.id
CategoryTheory.Equivalence.counitIso
Opposite.op
WalkingParallelPair.one
CategoryTheory.Iso.refl		——
walkingParallelPairOpEquiv_counitIso_zero 📖mathematical—CategoryTheory.Iso.app
Opposite
WalkingParallelPair
CategoryTheory.Category.opposite
walkingParallelPairHomCategory
CategoryTheory.Functor.comp
CategoryTheory.Equivalence.inverse
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.functor
CategoryTheory.Functor.id
CategoryTheory.Equivalence.counitIso
Opposite.op
WalkingParallelPair.zero
CategoryTheory.Iso.refl		——
walkingParallelPairOpEquiv_functor 📖mathematical—CategoryTheory.Equivalence.functor
WalkingParallelPair
Opposite
walkingParallelPairHomCategory
CategoryTheory.Category.opposite
walkingParallelPairOpEquiv
walkingParallelPairOp		——
walkingParallelPairOpEquiv_inverse 📖mathematical—CategoryTheory.Equivalence.inverse
WalkingParallelPair
Opposite
walkingParallelPairHomCategory
CategoryTheory.Category.opposite
walkingParallelPairOpEquiv
CategoryTheory.Functor.leftOp
walkingParallelPairOp		——
walkingParallelPairOpEquiv_unitIso_hom_app_one 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor.id
CategoryTheory.Functor.comp
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Equivalence.functor
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.inverse
CategoryTheory.Iso.hom
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.unitIso
WalkingParallelPair.one
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_unitIso_hom_app_zero 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor.id
CategoryTheory.Functor.comp
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Equivalence.functor
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.inverse
CategoryTheory.Iso.hom
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.unitIso
WalkingParallelPair.zero
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_unitIso_inv_app_one 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor.comp
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Equivalence.functor
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.inverse
CategoryTheory.Functor.id
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.unitIso
WalkingParallelPair.one
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_unitIso_inv_app_zero 📖mathematical—CategoryTheory.NatTrans.app
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor.comp
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Equivalence.functor
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.inverse
CategoryTheory.Functor.id
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Equivalence.unitIso
WalkingParallelPair.zero
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOpEquiv_unitIso_one 📖mathematical—CategoryTheory.Iso.app
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor.id
CategoryTheory.Functor.comp
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Equivalence.functor
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.inverse
CategoryTheory.Equivalence.unitIso
WalkingParallelPair.one
CategoryTheory.Iso.refl		——
walkingParallelPairOpEquiv_unitIso_zero 📖mathematical—CategoryTheory.Iso.app
WalkingParallelPair
walkingParallelPairHomCategory
CategoryTheory.Functor.id
CategoryTheory.Functor.comp
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Equivalence.functor
walkingParallelPairOpEquiv
CategoryTheory.Equivalence.inverse
CategoryTheory.Equivalence.unitIso
WalkingParallelPair.zero
CategoryTheory.Iso.refl		——
walkingParallelPairOp_left 📖mathematical—CategoryTheory.Functor.map
WalkingParallelPair
walkingParallelPairHomCategory
Opposite
CategoryTheory.Category.opposite
walkingParallelPairOp
WalkingParallelPair.zero
WalkingParallelPair.one
WalkingParallelPairHom.left
Quiver.Hom.op
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOp_one 📖mathematical—CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
Opposite
CategoryTheory.Category.opposite
walkingParallelPairOp
WalkingParallelPair.one
Opposite.op
WalkingParallelPair.zero		——
walkingParallelPairOp_right 📖mathematical—CategoryTheory.Functor.map
WalkingParallelPair
walkingParallelPairHomCategory
Opposite
CategoryTheory.Category.opposite
walkingParallelPairOp
WalkingParallelPair.zero
WalkingParallelPair.one
WalkingParallelPairHom.right
Quiver.Hom.op
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct		——
walkingParallelPairOp_zero 📖mathematical—CategoryTheory.Functor.obj
WalkingParallelPair
walkingParallelPairHomCategory
Opposite
CategoryTheory.Category.opposite
walkingParallelPairOp
WalkingParallelPair.zero
Opposite.op
WalkingParallelPair.one		——
ι_comp_coequalizerComparison 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
coequalizer
CategoryTheory.Functor.map
coequalizer.π
coequalizerComparison		—coequalizer.π_desc
ι_comp_coequalizerComparison_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
coequalizer
CategoryTheory.Functor.map
coequalizer.π
coequalizerComparison		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
ι_comp_coequalizerComparison

CategoryTheory.Limits.Cocone

Definitions

NameCategoryTheorems
ofCofork 📖CompOp
1 mathmath: ofCofork_ι

Theorems

NameKindAssumesProvesValidatesDepends On
ofCofork_ι 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
pt
ofCofork
ι
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor.map
CategoryTheory.Limits.WalkingParallelPairHom.left
CategoryTheory.Limits.WalkingParallelPairHom.right
CategoryTheory.eqToHom		——

CategoryTheory.Limits.Cofork

Definitions

NameCategoryTheorems
ext 📖CompOp
3 mathmath: CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, ext_inv, ext_hom
isColimitEquivOfIsos 📖CompOp—
isColimitOfIsos 📖CompOp—
isoCoforkOfπ 📖CompOp—
mkHom 📖CompOp
3 mathmath: mkHom_hom, ext_inv, ext_hom
ofCocone 📖CompOp
1 mathmath: ofCocone_ι
ofπ 📖CompOp
8 mathmath: CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_, π_ofπ, ofπ_pt, ofπ_ι_app, CategoryTheory.Limits.isCokernelEpiComp_desc
π 📖CompOp
76 mathmath: CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, CategoryTheory.Limits.Fork.π_comp_hom, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH, CategoryTheory.Monad.beckCoequalizer_desc, CategoryTheory.Limits.biprod.inlCokernelCofork_π, unop_op_π, CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right', CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_π, CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit, IsColimit.epi, condition_assoc, CategoryTheory.Limits.CokernelCofork.IsColimit.isIso_π, CategoryTheory.Limits.CokernelCofork.condition, app_zero_eq_comp_π_left, IsColimit.homIso_apply_coe, CategoryTheory.Limits.Multicofork.ofSigmaCofork_π, IsColimit.π_desc_assoc, CategoryTheory.Monad.MonadicityInternal.unitCofork_π, π_precompose, CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right, CategoryTheory.Preadditive.cokernelCoforkOfCofork_π, CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq, CategoryTheory.Limits.Fork.op_π, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_p, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd, CategoryTheory.Limits.Fork.π_comp_hom_assoc, condition, app_zero_eq_comp_π_right, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_π, CategoryTheory.IsSplitCoequalizer.asCofork_π, CategoryTheory.Limits.coconeOfIsSplitEpi_π, CategoryTheory.Limits.Multicofork.toSigmaCofork_π, CategoryTheory.Preadditive.coforkOfCokernelCofork_π, CategoryTheory.Limits.biprod.inrCokernelCofork_π, CategoryTheory.Limits.coequalizer.cofork_π, app_zero_eq_comp_π_right_assoc, CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit_assoc, CategoryTheory.Limits.BinaryBicone.inrCokernelCofork_π, CategoryTheory.Monad.beckCofork_π, CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app, CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv, IsColimit.existsUnique, CategoryTheory.Limits.CokernelCofork.condition_assoc, CategoryTheory.Limits.BinaryBicone.inlCokernelCofork_π, CategoryTheory.Limits.CokernelCofork.map_condition, CategoryTheory.Limits.CokernelCofork.map_π, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_π, op_unop_π, IsColimit.π_desc, TopCat.isOpen_iff_of_isColimit_cofork, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φQ, TopCat.isQuotientMap_of_isColimit_cofork, π_ofπ, CategoryTheory.Limits.CokernelCofork.π_ofπ, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom_assoc, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p, CategoryTheory.ShortComplex.exact_iff_of_forks, CategoryTheory.Limits.CokernelCofork.map_condition_assoc, IsColimit.homIso_symm_apply, IsColimit.π_desc', CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self, unop_ι, CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, IsColimit.π_desc'_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH, app_one_eq_π, CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom, CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app, op_ι, CategoryTheory.Limits.Fork.unop_π, CategoryTheory.Limits.isCokernelEpiComp_desc, CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi, CategoryTheory.Limits.epi_of_isColimit_cofork

Theorems

NameKindAssumesProvesValidatesDepends On
app_one_eq_π 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cocone.ι
CategoryTheory.Limits.WalkingParallelPair.one
π		——
app_zero_eq_comp_π_left 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cocone.ι
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.WalkingParallelPair.one
π		—app_one_eq_π
CategoryTheory.Limits.Cocone.w
CategoryTheory.Limits.parallelPair_map_left
app_zero_eq_comp_π_right 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cocone.ι
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.WalkingParallelPair.one
π		—app_one_eq_π
CategoryTheory.Limits.Cocone.w
CategoryTheory.Limits.parallelPair_map_right
app_zero_eq_comp_π_right_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.NatTrans.app
CategoryTheory.Limits.Cocone.ι
π		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
app_zero_eq_comp_π_right
coequalizer_ext 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
π		CategoryTheory.NatTrans.app
CategoryTheory.Limits.Cocone.ι		—app_zero_eq_comp_π_left
CategoryTheory.Category.assoc
condition 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
π		—app_zero_eq_comp_π_left
app_zero_eq_comp_π_right
condition_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
π		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
condition
ext_hom 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Limits.Cocone.pt
CategoryTheory.CategoryStruct.comp
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
π
CategoryTheory.Iso.hom		CategoryTheory.Limits.Cofork
CategoryTheory.Limits.Cocone.category
ext
mkHom		——
ext_inv 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Limits.Cocone.pt
CategoryTheory.CategoryStruct.comp
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
π
CategoryTheory.Iso.hom		CategoryTheory.Iso.inv
CategoryTheory.Limits.Cofork
CategoryTheory.Limits.Cocone.category
ext
mkHom		——
mkHom_hom 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
π		CategoryTheory.Limits.CoconeMorphism.hom
mkHom		——
ofCocone_ι 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor.map
CategoryTheory.Limits.WalkingParallelPairHom.left
CategoryTheory.Limits.WalkingParallelPairHom.right
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
ofCocone
CategoryTheory.Limits.Cocone.ι
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.eqToHom		——
ofπ_pt 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
ofπ		——
ofπ_ι_app 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.ι
ofπ
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.WalkingParallelPair.zero		——
π_ofπ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		π
ofπ		——
π_precompose 📖mathematical—π
CategoryTheory.Functor.obj
CategoryTheory.Limits.Cocone
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.Cocone.category
CategoryTheory.Limits.Cocones.precompose
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.NatTrans.app		——

CategoryTheory.Limits.Cofork.IsColimit

Definitions

NameCategoryTheorems
desc 📖CompOp
2 mathmath: π_desc', π_desc'_assoc
desc' 📖CompOp
1 mathmath: homIso_symm_apply
homIso 📖CompOp
8 mathmath: CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, homIso_apply_coe, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, homIso_natural, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, homIso_symm_apply
mk 📖CompOp—
mk' 📖CompOp—
ofExistsUnique 📖CompOp—

Theorems

NameKindAssumesProvesValidatesDepends On
epi 📖mathematical—CategoryTheory.Epi
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π		—hom_ext
existsUnique 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		ExistsUnique
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cofork.π		—CategoryTheory.Limits.IsColimit.fac
hom_ext
homIso_apply_coe 📖mathematical—Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
DFunLike.coe
Equiv
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
EquivLike.toFunLike
Equiv.instEquivLike
homIso
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Limits.Cofork.π		——
homIso_natural 📖mathematical—Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
DFunLike.coe
Equiv
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
EquivLike.toFunLike
Equiv.instEquivLike
homIso		—CategoryTheory.Category.assoc
homIso_symm_apply 📖mathematical—DFunLike.coe
Equiv
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
homIso
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cofork.π
desc'		——
hom_ext 📖—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π		——CategoryTheory.Limits.IsColimit.hom_ext
CategoryTheory.Limits.Cofork.coequalizer_ext
π_desc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π
CategoryTheory.Limits.IsColimit.desc		—CategoryTheory.Limits.IsColimit.fac
π_desc' 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π
desc		—CategoryTheory.Limits.IsColimit.fac
π_desc'_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π
desc		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
π_desc'
π_desc_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π
CategoryTheory.Limits.IsColimit.desc		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
π_desc

CategoryTheory.Limits.CoforkOfπ

Definitions

NameCategoryTheorems
ext 📖CompOp—

CategoryTheory.Limits.Cone

Definitions

NameCategoryTheorems
ofFork 📖CompOp
1 mathmath: ofFork_π

Theorems

NameKindAssumesProvesValidatesDepends On
ofFork_π 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
pt
ofFork
π
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor.map
CategoryTheory.Limits.WalkingParallelPairHom.left
CategoryTheory.Limits.WalkingParallelPairHom.right
CategoryTheory.eqToHom		——

CategoryTheory.Limits.Fork

Definitions

NameCategoryTheorems
equivOfIsos 📖CompOp
2 mathmath: equivOfIsos_functor_obj_ι, equivOfIsos_inverse_obj_ι
ext 📖CompOp
3 mathmath: CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, ext_hom, ext_inv
isLimitEquivOfIsos 📖CompOp—
isLimitOfIsos 📖CompOp—
isoForkOfι 📖CompOp
2 mathmath: isoForkOfι_hom_hom, isoForkOfι_inv_hom
mkHom 📖CompOp
3 mathmath: ext_hom, ext_inv, mkHom_hom
ofCone 📖CompOp
1 mathmath: ofCone_π
ofι 📖CompOp
16 mathmath: CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition, isoForkOfι_hom_hom, ofι_pt, CategoryTheory.Preadditive.kernelForkOfFork_ofι, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, ofι_π_app, CategoryTheory.Equalizer.Presieve.sheaf_condition, CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, CategoryTheory.Limits.isKernelCompMono_lift, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply, CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction, isoForkOfι_inv_hom, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, ι_ofι, CategoryTheory.Limits.Types.type_equalizer_iff_unique
ι 📖CompOp
87 mathmath: CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc, CategoryTheory.Limits.equalizer.fork_ι, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, IsLimit.lift_ι'_assoc, CategoryTheory.Subfunctor.Subpresheaf.equalizer.fork_ι, CategoryTheory.Limits.KernelFork.condition_assoc, CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι_assoc, isoForkOfι_hom_hom, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc, IsLimit.mono, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH, CategoryTheory.Limits.BinaryBicone.sndKernelFork_ι, CategoryTheory.Limits.KernelFork.ι_ofι, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl, CategoryTheory.Limits.coneOfIsSplitMono_ι, ι_postcompose, equivOfIsos_functor_obj_ι, IsLimit.existsUnique, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_ι, hom_comp_ι, CategoryTheory.Limits.biprod.fstKernelFork_ι, CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι, CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi, unop_op_ι, IsLimit.homIso_symm_apply, CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι, CommRingCat.instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_i, CategoryTheory.Limits.biprod.sndKernelFork_ι, CommRingCat.Under.tensorProdEqualizer_ι, hom_comp_ι_assoc, CategoryTheory.Limits.KernelFork.IsLimit.isIso_ι, CategoryTheory.Limits.KernelFork.condition, IsLimit.homIso_apply_coe, IsLimit.lift_ι, op_π, app_one_eq_ι_comp_left, CategoryTheory.Preadditive.kernelForkOfFork_ι, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH, app_one_eq_ι_comp_right_assoc, CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq, condition, app_zero_eq_ι, CategoryTheory.Limits.isKernelCompMono_lift, equivOfIsos_inverse_obj_ι, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, CategoryTheory.IsSplitEqualizer.asFork_ι, CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_ι, IsLimit.lift_ι_assoc, IsLimit.lift_ι', CategoryTheory.Limits.Multifork.ofPiFork_π_app_right, CategoryTheory.Limits.Multifork.ofPiFork_π_app_left, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles, CategoryTheory.Comonad.beckEqualizer_lift, CategoryTheory.Comonad.beckFork_ι, CommRingCat.Under.equalizerFork_ι, CategoryTheory.Limits.KernelFork.map_condition, CategoryTheory.Limits.BinaryBicone.fstKernelFork_ι, CategoryTheory.Preadditive.forkOfKernelFork_ι, CategoryTheory.Limits.KernelFork.map_ι, CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction, CategoryTheory.ShortComplex.exact_iff_of_forks, CategoryTheory.Limits.Multifork.ofPiFork_ι, op_unop_ι, condition_assoc, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, isoForkOfι_inv_hom, CategoryTheory.Limits.Cofork.unop_ι, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φK, CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i, CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj, ι_ofι, CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self, CategoryTheory.Subfunctor.equalizer.fork_ι, CategoryTheory.Limits.Multifork.toPiFork_π_app_zero, CategoryTheory.Limits.Cofork.op_ι, unop_π, CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι, app_one_eq_ι_comp_right, CommRingCat.Under.equalizerFork'_ι, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι, CategoryTheory.Limits.KernelFork.map_condition_assoc

Theorems

NameKindAssumesProvesValidatesDepends On
app_one_eq_ι_comp_left 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.Cone.π
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.WalkingParallelPair.zero
ι		—app_zero_eq_ι
CategoryTheory.Limits.Cone.w
CategoryTheory.Limits.parallelPair_map_left
app_one_eq_ι_comp_right 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.Cone.π
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.WalkingParallelPair.zero
ι		—app_zero_eq_ι
CategoryTheory.Limits.Cone.w
CategoryTheory.Limits.parallelPair_map_right
app_one_eq_ι_comp_right_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.NatTrans.app
CategoryTheory.Limits.Cone.π
CategoryTheory.Limits.WalkingParallelPair.zero
ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
app_one_eq_ι_comp_right
app_zero_eq_ι 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.Cone.π
CategoryTheory.Limits.WalkingParallelPair.zero
ι		——
condition 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.zero
ι		—app_one_eq_ι_comp_left
app_one_eq_ι_comp_right
condition_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.zero
ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
condition
equalizer_ext 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
ι		CategoryTheory.NatTrans.app
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.π		—app_one_eq_ι_comp_left
equivOfIsos_functor_obj_ι 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.Iso.hom		ι
CategoryTheory.Functor.obj
CategoryTheory.Limits.Fork
CategoryTheory.Limits.Cone.category
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Equivalence.functor
equivOfIsos
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair.zero		——
equivOfIsos_inverse_obj_ι 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.Iso.hom		ι
CategoryTheory.Functor.obj
CategoryTheory.Limits.Fork
CategoryTheory.Limits.Cone.category
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Equivalence.inverse
equivOfIsos
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Iso.inv		——
ext_hom 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.CategoryStruct.comp
CategoryTheory.Iso.hom
ι		CategoryTheory.Limits.Fork
CategoryTheory.Limits.Cone.category
ext
mkHom		——
ext_inv 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.CategoryStruct.comp
CategoryTheory.Iso.hom
ι		CategoryTheory.Iso.inv
CategoryTheory.Limits.Fork
CategoryTheory.Limits.Cone.category
ext
mkHom		——
hom_comp_ι 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.ConeMorphism.hom
ι		——
hom_comp_ι_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.ConeMorphism.hom
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
hom_comp_ι
isoForkOfι_hom_hom 📖mathematical—CategoryTheory.Limits.ConeMorphism.hom
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
ofι
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair.zero
ι
condition
CategoryTheory.Iso.hom
CategoryTheory.Limits.Fork
CategoryTheory.Limits.Cone.category
isoForkOfι
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		—condition
isoForkOfι_inv_hom 📖mathematical—CategoryTheory.Limits.ConeMorphism.hom
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
ofι
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair.zero
ι
condition
CategoryTheory.Iso.inv
CategoryTheory.Limits.Fork
CategoryTheory.Limits.Cone.category
isoForkOfι
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		—condition
mkHom_hom 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
ι		CategoryTheory.Limits.ConeMorphism.hom
mkHom		——
ofCone_π 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor.map
CategoryTheory.Limits.WalkingParallelPairHom.left
CategoryTheory.Limits.WalkingParallelPairHom.right
ofCone
CategoryTheory.Limits.Cone.π
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.eqToHom		——
ofι_pt 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
ofι		——
ofι_π_app 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.Cone.π
ofι
CategoryTheory.Limits.WalkingParallelPair.zero
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.WalkingParallelPair.one		——
ι_ofι 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		ι
ofι		——
ι_postcompose 📖mathematical—ι
CategoryTheory.Functor.obj
CategoryTheory.Limits.Cone
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.Cone.category
CategoryTheory.Limits.Cones.postcompose
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.NatTrans.app		——
π_comp_hom 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π
CategoryTheory.Limits.CoconeMorphism.hom		——
π_comp_hom_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.Cofork.π
CategoryTheory.Limits.CoconeMorphism.hom		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
π_comp_hom

CategoryTheory.Limits.Fork.IsLimit

Definitions

NameCategoryTheorems
homIso 📖CompOp
5 mathmath: homIso_natural, homIso_symm_apply, homIso_apply_coe, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply
lift' 📖CompOp
1 mathmath: homIso_symm_apply
mk 📖CompOp—
mk' 📖CompOp—
ofExistsUnique 📖CompOp—

Theorems

NameKindAssumesProvesValidatesDepends On
existsUnique 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		ExistsUnique
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.Fork.ι		—CategoryTheory.Limits.IsLimit.fac
hom_ext
homIso_apply_coe 📖mathematical—Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
DFunLike.coe
Equiv
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
EquivLike.toFunLike
Equiv.instEquivLike
homIso
CategoryTheory.Limits.Fork.ι		——
homIso_natural 📖mathematical—Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
DFunLike.coe
Equiv
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
EquivLike.toFunLike
Equiv.instEquivLike
homIso		—CategoryTheory.Category.assoc
homIso_symm_apply 📖mathematical—DFunLike.coe
Equiv
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.CategoryStruct.comp
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
homIso
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.Fork.ι
lift'		——
hom_ext 📖—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.Fork.ι		——CategoryTheory.Limits.IsLimit.hom_ext
CategoryTheory.Limits.Fork.equalizer_ext
lift_ι 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.IsLimit.lift
CategoryTheory.Limits.Fork.ι		—CategoryTheory.Limits.IsLimit.fac
lift_ι' 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
lift
CategoryTheory.Limits.Fork.ι		—CategoryTheory.Limits.IsLimit.fac
lift_ι'_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
lift
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.Fork.ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
lift_ι'
lift_ι_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.IsLimit.lift
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.Fork.ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
lift_ι
mk_lift 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.Fork.ι		CategoryTheory.Limits.IsLimit.lift——
mono 📖mathematical—CategoryTheory.Mono
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.Fork.ι		—hom_ext

CategoryTheory.Limits.ForkOfι

Definitions

NameCategoryTheorems
ext 📖CompOp—

CategoryTheory.Limits.WalkingParallelPairHom

Definitions

NameCategoryTheorems
comp 📖CompOp
3 mathmath: id_comp, comp_id, assoc

Theorems

NameKindAssumesProvesValidatesDepends On
assoc 📖mathematical—comp——
comp_id 📖mathematical—comp
id		——
id_comp 📖mathematical—comp
id		——

CategoryTheory.Limits.coequalizer

Definitions

NameCategoryTheorems
cofork 📖CompOp
2 mathmath: cofork_π, cofork_ι_app_one
desc 📖CompOp
15 mathmath: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, π_tensor_id_preserves_coequalizer_inv_desc, CategoryTheory.Limits.coequalizerComparison_map_desc, id_tensor_π_preserves_coequalizer_inv_desc, isoTargetOfSelf_hom, π_desc_assoc, CategoryTheory.Limits.coequalizerComparison_map_desc_assoc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc, π_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc_assoc, π_colimMap_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc_assoc, π_tensor_id_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.Regular.instMonoDesc
desc' 📖CompOp—
isoTargetOfSelf 📖CompOp
2 mathmath: isoTargetOfSelf_inv, isoTargetOfSelf_hom
π 📖CompOp
53 mathmath: π_of_self, Bimod.TensorBimod.π_tensor_id_actRight, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap, CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv, Bimod.TensorBimod.whiskerLeft_π_actLeft, TopCat.coequalizer_isOpen_iff, CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc, condition, π_epi, CategoryTheory.Limits.coequalizer_as_cokernel, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv_assoc, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, isoTargetOfSelf_inv, CategoryTheory.Limits.isPushout_coequalizer_coprod, CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv_apply, CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom, CategoryTheory.Monad.MonadicityInternal.unitCofork_π, π_tensor_id_preserves_coequalizer_inv_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_assoc, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, id_tensor_π_preserves_coequalizer_inv_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_assoc, cofork_π, CategoryTheory.Limits.ι_comp_coequalizerComparison_assoc, CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, CategoryTheory.Limits.ι_comp_coequalizerComparison, CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv, π_desc_assoc, hom_ext_iff, CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv, CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, condition_assoc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc, existsUnique, CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, cofork_ι_app_one, π_desc, CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, CategoryTheory.Limits.map_π_epi, CategoryTheory.Limits.map_π_preserves_coequalizer_inv, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc_assoc, CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc, π_of_eq, π_colimMap_desc, CategoryTheory.instIsRegularEpiπ, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc_assoc, π_tensor_id_preserves_coequalizer_inv_colimMap_desc

Theorems

NameKindAssumesProvesValidatesDepends On
cofork_ι_app_one 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cocone.pt
cofork
CategoryTheory.Limits.Cocone.ι
CategoryTheory.Limits.WalkingParallelPair.one
π		——
cofork_π 📖mathematical—CategoryTheory.Limits.Cofork.π
cofork
π		——
condition 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.coequalizer
π		—CategoryTheory.Limits.Cofork.condition
condition_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.coequalizer
π		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
condition
existsUnique 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		ExistsUnique
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.coequalizer
π		—CategoryTheory.Limits.Cofork.IsColimit.existsUnique
hom_ext 📖—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.coequalizer
π		——CategoryTheory.Limits.Cofork.IsColimit.hom_ext
hom_ext_iff 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.coequalizer
π		—hom_ext
isoTargetOfSelf_hom 📖mathematical—CategoryTheory.Iso.hom
CategoryTheory.Limits.coequalizer
CategoryTheory.Limits.hasCoequalizer_of_self
isoTargetOfSelf
desc
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		—hom_ext
CategoryTheory.Limits.hasCoequalizer_of_self
CategoryTheory.IsIso.hom_inv_id
π_of_self
CategoryTheory.Limits.colimit.ι_desc
isoTargetOfSelf_inv 📖mathematical—CategoryTheory.Iso.inv
CategoryTheory.Limits.coequalizer
CategoryTheory.Limits.hasCoequalizer_of_self
isoTargetOfSelf
π		—CategoryTheory.Limits.hasCoequalizer_of_self
π_colimMap_desc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.coequalizer
π
CategoryTheory.Limits.colimit
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Limits.colimMap
CategoryTheory.Limits.parallelPairHom
desc		—CategoryTheory.Limits.ι_colimMap_assoc
CategoryTheory.Limits.parallelPairHom_app_one
π_desc
π_desc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.coequalizer
π
desc		—CategoryTheory.Limits.colimit.ι_desc
π_desc_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.coequalizer
π
desc		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
π_desc
π_epi 📖mathematical—CategoryTheory.Epi
CategoryTheory.Limits.coequalizer
π		—hom_ext
π_of_eq 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Limits.coequalizer
π		—CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq
π_of_self 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Limits.coequalizer
CategoryTheory.Limits.hasCoequalizer_of_self
π		—π_of_eq
CategoryTheory.Limits.hasCoequalizer_of_self

CategoryTheory.Limits.equalizer

Definitions

NameCategoryTheorems
fork 📖CompOp
2 mathmath: fork_ι, fork_π_app_zero
isoSourceOfSelf 📖CompOp
2 mathmath: isoSourceOfSelf_hom, isoSourceOfSelf_inv
lift' 📖CompOp—
ι 📖CompOp
43 mathmath: ι_of_eq, fork_ι, CategoryTheory.Limits.equalizerComparison_comp_π, AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, CategoryTheory.Limits.equalizerSubobject_arrow'_assoc, lift_ι, CategoryTheory.Limits.isPullback_equalizer_prod, CategoryTheory.Limits.equalizer_as_kernel, AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated, AlgebraicGeometry.IsImmersion.instιScheme, CategoryTheory.instIsRegularMonoι, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst, CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι, condition, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst_assoc, CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι, CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype_apply, lift_ι_assoc, CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype, ι_mono, condition_assoc, CategoryTheory.Limits.PreservesEqualizer.iso_inv_ι, existsUnique, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc, CategoryTheory.Limits.equalizerSubobject_arrow, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst, AlgebraicGeometry.isClosedImmersion_equalizer_ι_left, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.Limits.equalizerSubobject_arrow', CategoryTheory.Limits.equalizerSubobject_arrow_assoc, ι_of_self, isoSourceOfSelf_hom, CategoryTheory.Limits.equalizerComparison_comp_π_assoc, fork_π_app_zero, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst_assoc, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux, CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply, hom_ext_iff, CategoryTheory.Limits.pullback_equalizer

Theorems

NameKindAssumesProvesValidatesDepends On
condition 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.equalizer
ι		—CategoryTheory.Limits.Fork.condition
condition_assoc 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.equalizer
ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
condition
existsUnique 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		ExistsUnique
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.equalizer
ι		—CategoryTheory.Limits.Fork.IsLimit.existsUnique
fork_ι 📖mathematical—CategoryTheory.Limits.Fork.ι
fork
ι		——
fork_π_app_zero 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Functor.obj
CategoryTheory.Functor
CategoryTheory.Functor.category
CategoryTheory.Functor.const
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.parallelPair
fork
CategoryTheory.Limits.Cone.π
CategoryTheory.Limits.WalkingParallelPair.zero
ι		——
hom_ext 📖—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.equalizer
ι		——CategoryTheory.Limits.Fork.IsLimit.hom_ext
hom_ext_iff 📖mathematical—CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.equalizer
ι		—hom_ext
isoSourceOfSelf_hom 📖mathematical—CategoryTheory.Iso.hom
CategoryTheory.Limits.equalizer
CategoryTheory.Limits.hasEqualizer_of_self
isoSourceOfSelf
ι		—CategoryTheory.Limits.hasEqualizer_of_self
isoSourceOfSelf_inv 📖mathematical—CategoryTheory.Iso.inv
CategoryTheory.Limits.equalizer
CategoryTheory.Limits.hasEqualizer_of_self
isoSourceOfSelf
lift
CategoryTheory.CategoryStruct.id
CategoryTheory.Category.toCategoryStruct		—hom_ext
CategoryTheory.Limits.hasEqualizer_of_self
CategoryTheory.IsIso.inv_hom_id
ι_of_self
CategoryTheory.Limits.limit.lift_π
lift_ι 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.equalizer
lift
ι		—CategoryTheory.Limits.limit.lift_π
lift_ι_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct		CategoryTheory.Limits.equalizer
lift
ι		—CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
lift_ι
ι_mono 📖mathematical—CategoryTheory.Mono
CategoryTheory.Limits.equalizer
ι		—hom_ext
ι_of_eq 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Limits.equalizer
ι		—CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq
ι_of_self 📖mathematical—CategoryTheory.IsIso
CategoryTheory.Limits.equalizer
CategoryTheory.Limits.hasEqualizer_of_self
ι		—ι_of_eq
CategoryTheory.Limits.hasEqualizer_of_self

CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom

Definitions

NameCategoryTheorems
decEq 📖CompOp—

CategoryTheory.Limits.instInhabitedWalkingParallelPair

Definitions

NameCategoryTheorems
default 📖CompOp—

CategoryTheory.Limits.parallelPair

Definitions

NameCategoryTheorems
eqOfHomEq 📖CompOp
2 mathmath: eqOfHomEq_hom_app, eqOfHomEq_inv_app
ext 📖CompOp
2 mathmath: ext_hom_app, ext_inv_app

Theorems

NameKindAssumesProvesValidatesDepends On
eqOfHomEq_hom_app 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Iso.hom
CategoryTheory.Functor
CategoryTheory.Functor.category
eqOfHomEq
CategoryTheory.Functor.obj
CategoryTheory.Iso
CategoryTheory.Iso.refl		——
eqOfHomEq_inv_app 📖mathematical—CategoryTheory.NatTrans.app
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
eqOfHomEq
CategoryTheory.Functor.obj
CategoryTheory.Iso
CategoryTheory.Iso.refl		——
ext_hom_app 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.CategoryStruct.comp
CategoryTheory.Functor.map
CategoryTheory.Limits.WalkingParallelPairHom.left
CategoryTheory.Iso.hom
CategoryTheory.Limits.WalkingParallelPairHom.right		CategoryTheory.NatTrans.app
CategoryTheory.Functor
CategoryTheory.Functor.category
ext
CategoryTheory.Iso		——
ext_inv_app 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.WalkingParallelPair.zero
CategoryTheory.Limits.WalkingParallelPair.one
CategoryTheory.CategoryStruct.comp
CategoryTheory.Functor.map
CategoryTheory.Limits.WalkingParallelPairHom.left
CategoryTheory.Iso.hom
CategoryTheory.Limits.WalkingParallelPairHom.right		CategoryTheory.NatTrans.app
CategoryTheory.Iso.inv
CategoryTheory.Functor
CategoryTheory.Functor.category
ext
CategoryTheory.Iso		——

---

← Back to Index