| Metric | Count |
Definitionscocones, cones, functorialityCompPostcompose, functorialityCompPrecompose, mapCocone, mapCoconeInv, mapCoconeInvMapCocone, mapCoconeMapCocone, mapCoconeMapCoconeInv, mapCoconeMorphism, mapCoconeOp, mapCoconePrecompose, mapCoconePrecomposeEquivalenceFunctor, mapCoconeWhisker, mapCone, mapConeInv, mapConeInvMapCone, mapConeMapCone, mapConeMapConeInv, mapConeMorphism, mapConeOp, mapConePostcompose, mapConePostcomposeEquivalenceFunctor, mapConeWhisker, postcomposeWhiskerLeftMapCone, precomposeWhiskerLeftMapCocone, Cocone, category, equiv, equivalenceOfReindexing, eta, ext, ext_inv, extend, extendComp, extendHom, extendId, extendIso, extensions, forget, functoriality, functorialityCompFunctoriality, functorialityEquivalence, op, precompose, precomposeComp, precomposeEquivalence, precomposeId, pt, unop, whisker, whiskering, whiskeringEquivalence, ΞΉ, CoconeMorphism, hom, equivalenceOfReindexing, eta, ext, extend, extendComp, extendId, extendIso, forget, functoriality, functorialityCompFunctoriality, functorialityEquivalence, postcompose, postcomposeComp, postcomposeEquivalence, postcomposeId, whiskering, whiskeringEquivalence, category, equiv, equivalenceOfReindexing, eta, ext, ext_inv, extend, extendComp, extendHom, extendId, extendIso, extensions, forget, functoriality, functorialityCompFunctoriality, functorialityEquivalence, op, postcompose, postcomposeComp, postcomposeEquivalence, postcomposeId, pt, unop, whisker, whiskering, whiskeringEquivalence, Ο, ConeMorphism, hom, equivalenceOfReindexing, eta, ext, extend, extendComp, extendId, extendIso, forget, functoriality, functorialityCompFunctoriality, functorialityEquivalence, postcompose, postcomposeComp, postcomposeEquivalence, postcomposeId, whiskering, whiskeringEquivalence, coconeEquivalenceOpConeOp, coconeLeftOpOfCone, coconeLeftOpOfConeEquiv, coconeOfConeLeftOp, coconeOfConeRightOp, coconeOfConeUnop, coconeOpEquiv, coconeRightOpOfCone, coconeRightOpOfConeEquiv, coconeUnopOfCone, coconeUnopOfConeEquiv, coneEquivalenceOpCoconeOp, coneLeftOpOfCocone, coneLeftOpOfCoconeEquiv, coneOfCoconeLeftOp, coneOfCoconeRightOp, coneOfCoconeUnop, coneOpEquiv, coneRightOpOfCocone, coneRightOpOfCoconeEquiv, coneUnopOfCocone, coneUnopOfCoconeEquiv, inhabitedCocone, inhabitedCoconeMorphism, inhabitedCone, inhabitedConeMorphism, cocones, cones | 147 |
Theoremscocones_map_app, cocones_obj, cones_map_app, cones_obj, functorialityCompPostcompose_hom_app_hom, functorialityCompPostcompose_inv_app_hom, functorialityCompPrecompose_hom_app_hom, functorialityCompPrecompose_inv_app_hom, mapCoconeMapCocone_hom_hom, mapCoconeMapCocone_inv_hom, mapCoconeOp_hom_hom, mapCoconeOp_inv_hom, mapCoconePrecomposeEquivalenceFunctor_hom_hom, mapCoconePrecomposeEquivalenceFunctor_inv_hom, mapCoconePrecompose_hom_hom, mapCoconePrecompose_inv_hom, mapCoconeWhisker_hom_hom, mapCoconeWhisker_inv_hom, mapCocone_pt, mapCocone_ΞΉ_app, mapConeMapCone_hom_hom, mapConeMapCone_inv_hom, mapConeOp_hom_hom, mapConeOp_inv_hom, mapConePostcomposeEquivalenceFunctor_hom_hom, mapConePostcomposeEquivalenceFunctor_inv_hom, mapConePostcompose_hom_hom, mapConePostcompose_inv_hom, mapConeWhisker_hom_hom, mapConeWhisker_inv_hom, mapCone_pt, mapCone_Ο_app, postcomposeWhiskerLeftMapCone_hom_hom, postcomposeWhiskerLeftMapCone_inv_hom, precomposeWhiskerLeftMapCocone_hom_hom, precomposeWhiskerLeftMapCocone_inv_hom, category_comp_hom, category_id_hom, cocone_iso_of_hom_iso, equivalenceOfReindexing_counitIso, equivalenceOfReindexing_functor, equivalenceOfReindexing_inverse, equivalenceOfReindexing_unitIso, eta_hom_hom, eta_inv_hom, ext_hom_hom, ext_inv_hom, ext_inv_hom_hom, ext_inv_inv_hom, extendComp_hom_hom, extendComp_inv_hom, extendHom_hom, extendId_hom_hom, extendId_inv_hom, extendIso_hom_hom, extendIso_inv_hom, extend_pt, extend_ΞΉ, extensions_app, forget_map, forget_obj, functorialityEquivalence_counitIso, functorialityEquivalence_functor, functorialityEquivalence_inverse, functorialityEquivalence_unitIso, functoriality_faithful, functoriality_full, functoriality_map_hom, functoriality_obj_pt, functoriality_obj_ΞΉ_app, instIsIsoExtendHom, op_pt, op_Ο, precomposeComp_hom_app_hom, precomposeComp_inv_app_hom, precomposeEquivalence_counitIso, precomposeEquivalence_functor, precomposeEquivalence_inverse, precomposeEquivalence_unitIso, precomposeId_hom_app_hom, precomposeId_inv_app_hom, precompose_map_hom, precompose_obj_pt, precompose_obj_ΞΉ, reflects_cocone_isomorphism, unop_pt, unop_Ο, w, w_assoc, whisker_pt, whisker_ΞΉ, whiskeringEquivalence_counitIso, whiskeringEquivalence_functor, whiskeringEquivalence_inverse, whiskeringEquivalence_unitIso, whiskering_map_hom, whiskering_obj, ext, ext_iff, hom_inv_id, hom_inv_id_assoc, inv_hom_id, inv_hom_id_assoc, map_w, map_w_assoc, w, w_assoc, cone_iso_of_hom_iso, functoriality_faithful, functoriality_full, reflects_cone_isomorphism, category_comp_hom, category_id_hom, cone_iso_of_hom_iso, equiv_hom_fst, equiv_hom_snd, equiv_inv_pt, equiv_inv_Ο, equivalenceOfReindexing_counitIso, equivalenceOfReindexing_functor, equivalenceOfReindexing_inverse, equivalenceOfReindexing_unitIso, eta_hom_hom, eta_inv_hom, ext_hom_hom, ext_inv_hom, ext_inv_hom_hom, ext_inv_inv_hom, extendComp_hom_hom, extendComp_inv_hom, extendHom_hom, extendId_hom_hom, extendId_inv_hom, extendIso_hom_hom, extendIso_inv_hom, extend_pt, extend_Ο, extensions_app, forget_map, forget_obj, functorialityEquivalence_counitIso, functorialityEquivalence_functor, functorialityEquivalence_inverse, functorialityEquivalence_unitIso, functoriality_faithful, functoriality_full, functoriality_map_hom, functoriality_obj_pt, functoriality_obj_Ο_app, instIsIsoExtendHom, op_pt, op_ΞΉ, postcomposeComp_hom_app_hom, postcomposeComp_inv_app_hom, postcomposeEquivalence_counitIso, postcomposeEquivalence_functor, postcomposeEquivalence_inverse, postcomposeEquivalence_unitIso, postcomposeId_hom_app_hom, postcomposeId_inv_app_hom, postcompose_map_hom, postcompose_obj_pt, postcompose_obj_Ο, reflects_cone_isomorphism, unop_pt, unop_ΞΉ, w, w_assoc, whisker_pt, whisker_Ο, whiskeringEquivalence_counitIso, whiskeringEquivalence_functor, whiskeringEquivalence_inverse, whiskeringEquivalence_unitIso, whiskering_map_hom, whiskering_obj, ext, ext_iff, hom_inv_id, hom_inv_id_assoc, inv_hom_id, inv_hom_id_assoc, map_w, map_w_assoc, w, w_assoc, cone_iso_of_hom_iso, functoriality_faithful, functoriality_full, reflects_cone_isomorphism, coconeLeftOpOfConeEquiv_counitIso, coconeLeftOpOfConeEquiv_functor_map_hom, coconeLeftOpOfConeEquiv_functor_obj, coconeLeftOpOfConeEquiv_inverse_map, coconeLeftOpOfConeEquiv_inverse_obj, coconeLeftOpOfConeEquiv_unitIso, coconeLeftOpOfCone_pt, coconeLeftOpOfCone_ΞΉ_app, coconeOfConeLeftOp_pt, coconeOfConeLeftOp_ΞΉ_app, coconeOfConeRightOp_pt, coconeOfConeRightOp_ΞΉ, coconeOfConeUnop_pt, coconeOfConeUnop_ΞΉ, coconeOpEquiv_counitIso, coconeOpEquiv_functor_map_hom, coconeOpEquiv_functor_obj, coconeOpEquiv_inverse_map, coconeOpEquiv_inverse_obj, coconeOpEquiv_unitIso, coconeRightOpOfConeEquiv_counitIso, coconeRightOpOfConeEquiv_functor_map_hom, coconeRightOpOfConeEquiv_functor_obj, coconeRightOpOfConeEquiv_inverse_map, coconeRightOpOfConeEquiv_inverse_obj, coconeRightOpOfConeEquiv_unitIso, coconeRightOpOfCone_pt, coconeRightOpOfCone_ΞΉ, coconeUnopOfConeEquiv_counitIso, coconeUnopOfConeEquiv_functor_map_hom, coconeUnopOfConeEquiv_functor_obj, coconeUnopOfConeEquiv_inverse_map, coconeUnopOfConeEquiv_inverse_obj, coconeUnopOfConeEquiv_unitIso, coconeUnopOfCone_pt, coconeUnopOfCone_ΞΉ, coneLeftOpOfCoconeEquiv_counitIso, coneLeftOpOfCoconeEquiv_functor_map_hom, coneLeftOpOfCoconeEquiv_functor_obj, coneLeftOpOfCoconeEquiv_inverse_map, coneLeftOpOfCoconeEquiv_inverse_obj, coneLeftOpOfCoconeEquiv_unitIso, coneLeftOpOfCocone_pt, coneLeftOpOfCocone_Ο_app, coneOfCoconeLeftOp_pt, coneOfCoconeLeftOp_Ο_app, coneOfCoconeRightOp_pt, coneOfCoconeRightOp_Ο, coneOfCoconeUnop_pt, coneOfCoconeUnop_Ο, coneOpEquiv_counitIso, coneOpEquiv_functor_map_hom, coneOpEquiv_functor_obj, coneOpEquiv_inverse_map, coneOpEquiv_inverse_obj, coneOpEquiv_unitIso, coneRightOpOfCoconeEquiv_counitIso, coneRightOpOfCoconeEquiv_functor_map_hom, coneRightOpOfCoconeEquiv_functor_obj, coneRightOpOfCoconeEquiv_inverse_map, coneRightOpOfCoconeEquiv_inverse_obj, coneRightOpOfCoconeEquiv_unitIso, coneRightOpOfCocone_pt, coneRightOpOfCocone_Ο, coneUnopOfCoconeEquiv_counitIso, coneUnopOfCoconeEquiv_functor_map_hom, coneUnopOfCoconeEquiv_functor_obj, coneUnopOfCoconeEquiv_inverse_map, coneUnopOfCoconeEquiv_inverse_obj, coneUnopOfCoconeEquiv_unitIso, coneUnopOfCocone_pt, coneUnopOfCocone_Ο, instIsIsoHomHomCocone, instIsIsoHomHomCone, instIsIsoHomInvCocone, instIsIsoHomInvCone, cocones_map_app_app, cocones_obj_map_app, cocones_obj_obj, cones_map_app_app, cones_obj_map_app, cones_obj_obj | 272 |
| Total | 419 |
| Name | Category | Theorems |
cocones π | CompOp | 6 mathmath: CategoryTheory.Limits.yonedaCompLimIsoCocones_inv_app, CategoryTheory.Limits.colimit.homIso_hom, CategoryTheory.Limits.yonedaCompLimIsoCocones_hom_app_app, cocones_obj, cocones_map_app, CategoryTheory.Limits.Cocone.extensions_app
|
cones π | CompOp | 10 mathmath: CategoryTheory.Limits.Cone.equiv_inv_pt, cones_map_app, CategoryTheory.Limits.coyonedaCompLimIsoCones_inv_app, cones_obj, CategoryTheory.Limits.Cone.equiv_hom_fst, CategoryTheory.Limits.Cone.equiv_inv_Ο, CategoryTheory.Limits.Cone.equiv_hom_snd, CategoryTheory.Limits.limit.homIso_hom, CategoryTheory.Limits.Cone.extensions_app, CategoryTheory.Limits.coyonedaCompLimIsoCones_hom_app_app
|
functorialityCompPostcompose π | CompOp | 2 mathmath: functorialityCompPostcompose_hom_app_hom, functorialityCompPostcompose_inv_app_hom
|
functorialityCompPrecompose π | CompOp | 2 mathmath: functorialityCompPrecompose_hom_app_hom, functorialityCompPrecompose_inv_app_hom
|
mapCocone π | CompOp | 47 mathmath: mapCocone_ΞΉ_app, mapCoconePrecomposeEquivalenceFunctor_inv_hom, mapCoconePrecompose_inv_hom, mapCoconeWhisker_hom_hom, LeftExtension.coconeAtWhiskerRightIso_inv_hom, mapCoconeOp_inv_hom, CategoryTheory.preservesColimitIso_inv_comp_desc, mapCoconeMapCocone_hom_hom, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, Condensed.isColimitLocallyConstantPresheaf_desc_apply, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, CategoryTheory.TransfiniteCompositionOfShape.map_isColimit, CategoryTheory.Limits.PreservesColimit.preserves, CategoryTheory.IsVanKampenColimit.map_reflective, CategoryTheory.IsUniversalColimit.map_reflective, CategoryTheory.Comma.coconeOfPreserves_ΞΉ_app_right, precomposeWhiskerLeftMapCocone_hom_hom, CategoryTheory.Comma.coconeOfPreserves_pt_hom, precomposeWhiskerLeftMapCocone_inv_hom, mapCoconePrecomposeEquivalenceFunctor_hom_hom, Accessible.Limits.isColimitMapCocone.surjective, CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ΞΉ_app, CategoryTheory.preservesColimitIso_inv_comp_desc_assoc, CategoryTheory.Comma.coconeOfPreserves_ΞΉ_app_left, LeftExtension.coconeAtWhiskerRightIso_hom_hom, SheafOfModules.Presentation.map_relations_I, mapCoconeWhisker_inv_hom, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.Cocone.mapCoconeToOver_inv_hom, mapConeOp_inv_hom, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f, mapCoconeOp_hom_hom, AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.colimit.post_desc, mapCoconePrecompose_hom_hom, CategoryTheory.IsVanKampenColimit.mapCocone_iff, mapConeOp_hom_hom, CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt, mapCocone_pt, CategoryTheory.Limits.Cocone.mapCoconeToOver_hom_hom, CategoryTheory.preserves_desc_mapCocone, mapCoconeMapCocone_inv_hom, CategoryTheory.Comma.colimitAuxiliaryCocone_ΞΉ_app, AlgebraicGeometry.nonempty_isColimit_Ξ_mapCocone, CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f
|
mapCoconeInv π | CompOp | β |
mapCoconeInvMapCocone π | CompOp | β |
mapCoconeMapCocone π | CompOp | 2 mathmath: mapCoconeMapCocone_hom_hom, mapCoconeMapCocone_inv_hom
|
mapCoconeMapCoconeInv π | CompOp | β |
mapCoconeMorphism π | CompOp | β |
mapCoconeOp π | CompOp | 2 mathmath: mapCoconeOp_inv_hom, mapCoconeOp_hom_hom
|
mapCoconePrecompose π | CompOp | 2 mathmath: mapCoconePrecompose_inv_hom, mapCoconePrecompose_hom_hom
|
mapCoconePrecomposeEquivalenceFunctor π | CompOp | 2 mathmath: mapCoconePrecomposeEquivalenceFunctor_inv_hom, mapCoconePrecomposeEquivalenceFunctor_hom_hom
|
mapCoconeWhisker π | CompOp | 2 mathmath: mapCoconeWhisker_hom_hom, mapCoconeWhisker_inv_hom
|
mapCone π | CompOp | 59 mathmath: mapConeMapCone_hom_hom, CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_hom, CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f, CategoryTheory.Limits.PreservesLimit.preserves, CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_hom, CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, CategoryTheory.CostructuredArrow.CreatesConnected.mapCone_raiseCone, mapConePostcompose_inv_hom, CategoryTheory.Comma.coneOfPreserves_Ο_app_right, CategoryTheory.Mon.limitConeIsLimit_lift_hom, CategoryTheory.Limits.limit.lift_post, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, mapCoconeOp_inv_hom, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, CategoryTheory.lift_comp_preservesLimitIso_hom_assoc, CategoryTheory.Limits.Cone.toStructuredArrowCone_Ο_app, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, RightExtension.coneAtWhiskerRightIso_inv_hom, postcomposeWhiskerLeftMapCone_inv_hom, CategoryTheory.lift_comp_preservesLimitIso_hom, CategoryTheory.Limits.Cone.mapConeToUnder_inv_hom, CategoryTheory.Comma.limitAuxiliaryCone_Ο_app, CategoryTheory.Presheaf.isSheaf_iff_isLimit, mapCone_pt, CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso, CategoryTheory.liftedLimitMapsToOriginal_inv_map_Ο, mapConePostcomposeEquivalenceFunctor_inv_hom, mapConePostcomposeEquivalenceFunctor_hom_hom, mapCone_Ο_app, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isLimit, mapConeWhisker_hom_hom, CategoryTheory.Comma.coneOfPreserves_pt_hom, postcomposeWhiskerLeftMapCone_hom_hom, mapConeOp_inv_hom, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, mapConePostcompose_hom_hom, TopCat.Presheaf.isGluing_iff_pairwise, RightExtension.coneAtWhiskerRightIso_hom_hom, mapCoconeOp_hom_hom, CategoryTheory.Limits.Cone.mapConeToUnder_hom_hom, mapConeOp_hom_hom, mapConeMapCone_inv_hom, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.preserves_lift_mapCone, mapConeWhisker_inv_hom, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, CategoryTheory.liftedLimitMapsToOriginal_hom_Ο, CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone, CategoryTheory.PreservesFiniteLimitsOfFlat.fac, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit_lift_f, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, CategoryTheory.Limits.Cone.toStructuredArrowCone_pt, FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology, CategoryTheory.Comma.coneOfPreserves_Ο_app_left
|
mapConeInv π | CompOp | β |
mapConeInvMapCone π | CompOp | β |
mapConeMapCone π | CompOp | 2 mathmath: mapConeMapCone_hom_hom, mapConeMapCone_inv_hom
|
mapConeMapConeInv π | CompOp | β |
mapConeMorphism π | CompOp | β |
mapConeOp π | CompOp | 2 mathmath: mapConeOp_inv_hom, mapConeOp_hom_hom
|
mapConePostcompose π | CompOp | 2 mathmath: mapConePostcompose_inv_hom, mapConePostcompose_hom_hom
|
mapConePostcomposeEquivalenceFunctor π | CompOp | 2 mathmath: mapConePostcomposeEquivalenceFunctor_inv_hom, mapConePostcomposeEquivalenceFunctor_hom_hom
|
mapConeWhisker π | CompOp | 2 mathmath: mapConeWhisker_hom_hom, mapConeWhisker_inv_hom
|
postcomposeWhiskerLeftMapCone π | CompOp | 2 mathmath: postcomposeWhiskerLeftMapCone_inv_hom, postcomposeWhiskerLeftMapCone_hom_hom
|
precomposeWhiskerLeftMapCocone π | CompOp | 2 mathmath: precomposeWhiskerLeftMapCocone_hom_hom, precomposeWhiskerLeftMapCocone_inv_hom
|
| Name | Category | Theorems |
Cocone π | CompData | 205 mathmath: CategoryTheory.Functor.LeftExtension.coconeAtFunctor_map_hom, Cocone.category_id_hom, IsColimit.uniqueUpToIso_hom, coneOpEquiv_unitIso, coconeLeftOpOfConeEquiv_functor_map_hom, coneRightOpOfCoconeEquiv_functor_obj, Cocone.whiskeringEquivalence_counitIso, coneRightOpOfCoconeEquiv_functor_map_hom, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, coneUnopOfCoconeEquiv_counitIso, CategoryTheory.WithInitial.coconeEquiv_functor_obj_pt, Cocone.equivalenceOfReindexing_inverse, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom, CategoryTheory.Functor.mapCoconePrecompose_inv_hom, PushoutCocone.unop_Ο_app, Types.isColimit_iff_coconeTypesIsColimit, CategoryTheory.Functor.mapCoconeWhisker_hom_hom, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_right, Cocone.extendComp_inv_hom, CategoryTheory.Functor.Final.colimitCoconeOfComp_isColimit, CategoryTheory.Functor.Final.coconesEquiv_unitIso, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, coconeUnopOfConeEquiv_unitIso, Cocone.extendIso_inv_hom, instIsIsoHomHomCocone, PushoutCocone.isoMk_inv_hom, Cocone.equivalenceOfReindexing_functor, colimit.map_desc, CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app, CategoryTheory.Functor.Final.coconesEquiv_functor, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_hom, CoconeMorphism.hom_inv_id_assoc, coconeLeftOpOfConeEquiv_inverse_obj, Cocone.functorialityEquivalence_counitIso, coconeRightOpOfConeEquiv_functor_map_hom, coneRightOpOfCoconeEquiv_inverse_obj, CategoryTheory.Functor.coconeTypesEquiv_apply_pt, Cocone.extendIso_hom_hom, Cocone.functorialityEquivalence_unitIso, Cocone.category_comp_hom, CategoryTheory.IsUniversalColimit.precompose_isIso, HasColimit.isoOfNatIso_inv_desc_assoc, IsColimit.ofCoconeEquiv_symm_apply_desc, HasColimit.isoOfNatIso_hom_desc, Cocone.equivalenceOfReindexing_counitIso, IsInitial.to_eq_descCoconeMorphism, Cocone.functoriality_obj_ΞΉ_app, coneOpEquiv_inverse_obj, DiagramOfCocones.coconePoints_map, CategoryTheory.WithInitial.coconeEquiv_counitIso_inv_app_hom, coconeUnopOfConeEquiv_counitIso, CategoryTheory.Functor.coconeTypesEquiv_symm_apply_pt, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_star, coconeUnopOfConeEquiv_functor_obj, CategoryTheory.Adjunction.functorialityUnit_app_hom, Cocone.cocone_iso_of_hom_iso, CategoryTheory.WithInitial.coconeEquiv_unitIso_hom_app_hom_right, CategoryTheory.Functor.mapCoconeMapCocone_hom_hom, Cocone.precomposeComp_hom_app_hom, Cocone.functoriality_map_hom, coconeUnopOfConeEquiv_functor_map_hom, Cocone.extendId_inv_hom, CategoryTheory.IsFiltered.cocone_nonempty, coconeOpEquiv_inverse_map, Cocone.reflects_cocone_isomorphism, Cocone.whiskering_map_hom, coconeOpEquiv_functor_obj, CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom, Cocone.toStructuredArrow_obj, CategoryTheory.IsCardinalFiltered.nonempty_cocone, coconeUnopOfConeEquiv_inverse_map, CategoryTheory.IsVanKampenColimit.precompose_isIso, CategoryTheory.WithInitial.coconeEquiv_functor_map_hom, IsColimit.coconePointsIsoOfEquivalence_hom, Cocone.precomposeId_hom_app_hom, DiagramOfCocones.comp, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_left_as, Cofork.Ο_precompose, Cocone.precomposeEquivalence_counitIso, Cocone.equivStructuredArrow_unitIso, coneLeftOpOfCoconeEquiv_inverse_obj, Cocone.precompose_map_hom, Cocones.cone_iso_of_hom_iso, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom, CategoryTheory.IsFiltered.iff_cocone_nonempty, Cocone.fromStructuredArrow_obj_pt, coconeRightOpOfConeEquiv_inverse_obj, Cocone.forget_map, DiagramOfCocones.mkOfHasColimits_map_hom, coneOpEquiv_functor_obj, coconeRightOpOfConeEquiv_unitIso, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ΞΉ_app_right, coneOpEquiv_counitIso, coneUnopOfCoconeEquiv_functor_map_hom, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom, Cocone.functorialityEquivalence_inverse, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom, CategoryTheory.Adjunction.functorialityCounit_app_hom, IsColimit.coconePointsIsoOfEquivalence_inv, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_of, CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ΞΉ, reflexiveCoforkEquivCofork_functor_obj_pt, IsColimit.descCoconeMorphism_eq_isInitial_to, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app', Cocone.precomposeId_inv_app_hom, coconeRightOpOfConeEquiv_inverse_map, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, CategoryTheory.Functor.LeftExtension.coconeAtFunctor_obj, coneRightOpOfCoconeEquiv_inverse_map, CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom, Cocone.precompose_obj_ΞΉ, SheafOfModules.Presentation.map_relations_I, coneUnopOfCoconeEquiv_functor_obj, reflexiveCoforkEquivCofork_inverse_obj_pt, coneUnopOfCoconeEquiv_inverse_obj, Cocone.eta_inv_hom, Cocones.reflects_cone_isomorphism, IsColimit.ofCoconeEquiv_apply_desc, coconeLeftOpOfConeEquiv_unitIso, CategoryTheory.Functor.coconeTypesEquiv_apply_ΞΉ_app, Cocones.functoriality_faithful, CategoryTheory.Functor.mapCoconeWhisker_inv_hom, coconeOpEquiv_inverse_obj, Cocone.fromStructuredArrow_map_hom, Cocone.ext_hom_hom, CoconeMorphism.hom_inv_id, HasColimit.isoOfNatIso_hom_desc_assoc, coneOpEquiv_functor_map_hom, Cocones.functoriality_full, Cocone.ext_inv_hom_hom, Cocone.functoriality_obj_pt, Cocone.forget_obj, coconeOpEquiv_unitIso, Cocone.whiskeringEquivalence_inverse, Cocone.precomposeEquivalence_functor, pointwiseBinaryBicone.isBilimit_isColimit, coneLeftOpOfCoconeEquiv_functor_map_hom, Cocone.functorialityEquivalence_functor, coneLeftOpOfCoconeEquiv_functor_obj, Cocone.equivStructuredArrow_inverse, coneLeftOpOfCoconeEquiv_unitIso, CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right, coneLeftOpOfCoconeEquiv_inverse_map, coconeRightOpOfConeEquiv_counitIso, Cocone.mapCoconeToOver_inv_hom, coconeRightOpOfConeEquiv_functor_obj, IsColimit.equivIsoColimit_symm_apply, colimit.map_desc_assoc, Cocone.precomposeEquivalence_unitIso, CategoryTheory.Functor.mapConeOp_inv_hom, CategoryTheory.Functor.Final.coconesEquiv_counitIso, IsColimit.hom_isIso, IsColimit.uniqueUpToIso_inv, coneOpEquiv_inverse_map, coconeUnopOfConeEquiv_inverse_obj, CoconeMorphism.inv_hom_id, Cocone.ext_inv_hom, CategoryTheory.WithInitial.coconeEquiv_counitIso_hom_app_hom, CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom, DiagramOfCocones.id, IsColimit.ofIsoColimit_desc, Cocone.functoriality_faithful, Cocone.whiskeringEquivalence_unitIso, coneLeftOpOfCoconeEquiv_counitIso, PushoutCocone.isoMk_hom_hom, Cocone.whiskering_obj, CategoryTheory.Functor.mapCoconePrecompose_hom_hom, hasColimit_iff_hasInitial_cocone, Cocone.equivalenceOfReindexing_unitIso, Cocone.functoriality_full, Cocone.extendComp_hom_hom, CategoryTheory.Functor.mapConeOp_hom_hom, coneUnopOfCoconeEquiv_inverse_map, Cocone.toStructuredArrow_map, coconeOpEquiv_counitIso, CategoryTheory.Functor.Final.extendCocone_obj_pt, Cocone.ext_inv_inv_hom, coconeLeftOpOfConeEquiv_counitIso, Cocone.precomposeEquivalence_inverse, instIsIsoHomInvCocone, CategoryTheory.Functor.Final.extendCocone_map_hom, Cocone.mapCoconeToOver_hom_hom, coneRightOpOfCoconeEquiv_unitIso, CoconeMorphism.inv_hom_id_assoc, Cocone.eta_hom_hom, CategoryTheory.Functor.CoconeTypes.isColimit_iff, Cocone.precomposeComp_inv_app_hom, Cocone.equivStructuredArrow_functor, Cocone.fromStructuredArrow_obj_ΞΉ, Cocone.equivStructuredArrow_counitIso, CategoryTheory.Functor.mapCoconeMapCocone_inv_hom, Cocone.extendId_hom_hom, coconeLeftOpOfConeEquiv_inverse_map, HasColimit.isoOfNatIso_inv_desc, CategoryTheory.WithInitial.coconeEquiv_unitIso_inv_app_hom_right, coconeOpEquiv_functor_map_hom, Cocone.instIsIsoExtendHom, CategoryTheory.Functor.Final.coconesEquiv_inverse, Cocone.whiskeringEquivalence_functor, coneUnopOfCoconeEquiv_unitIso, coconeLeftOpOfConeEquiv_functor_obj, Cocone.precompose_obj_pt, coneRightOpOfCoconeEquiv_counitIso, CategoryTheory.Functor.Final.colimitCoconeOfComp_cocone
|
CoconeMorphism π | CompData | β |
ConeMorphism π | CompData | β |
coconeEquivalenceOpConeOp π | CompOp | β |
coconeLeftOpOfCone π | CompOp | 8 mathmath: coconeLeftOpOfConeEquiv_functor_map_hom, isColimitCoconeLeftOpOfCone_desc, isLimitOfCoconeLeftOpOfCone_lift, isLimitConeOfCoconeLeftOp_lift, coconeLeftOpOfCone_ΞΉ_app, coconeLeftOpOfConeEquiv_counitIso, coconeLeftOpOfConeEquiv_functor_obj, coconeLeftOpOfCone_pt
|
coconeLeftOpOfConeEquiv π | CompOp | 6 mathmath: coconeLeftOpOfConeEquiv_functor_map_hom, coconeLeftOpOfConeEquiv_inverse_obj, coconeLeftOpOfConeEquiv_unitIso, coconeLeftOpOfConeEquiv_counitIso, coconeLeftOpOfConeEquiv_inverse_map, coconeLeftOpOfConeEquiv_functor_obj
|
coconeOfConeLeftOp π | CompOp | 8 mathmath: coconeOfConeLeftOp_pt, isLimitOfCoconeOfConeLeftOp_lift, coneLeftOpOfCoconeEquiv_inverse_obj, isLimitConeLeftOpOfCocone_lift, coneLeftOpOfCoconeEquiv_inverse_map, coconeOfConeLeftOp_ΞΉ_app, coneLeftOpOfCoconeEquiv_counitIso, isColimitCoconeOfConeLeftOp_desc
|
coconeOfConeRightOp π | CompOp | 8 mathmath: isLimitConeRightOpOfCocone_lift, isLimitOfCoconeOfConeRightOp_lift, coneRightOpOfCoconeEquiv_inverse_obj, coconeOfConeRightOp_ΞΉ, coconeOfConeRightOp_pt, coneRightOpOfCoconeEquiv_inverse_map, isColimitCoconeOfConeRightOp_desc, coneRightOpOfCoconeEquiv_counitIso
|
coconeOfConeUnop π | CompOp | 8 mathmath: coneUnopOfCoconeEquiv_counitIso, coconeOfConeUnop_pt, isLimitConeUnopOfCocone_lift, coneUnopOfCoconeEquiv_inverse_obj, isLimitOfCoconeOfConeUnop_lift, coconeOfConeUnop_ΞΉ, coneUnopOfCoconeEquiv_inverse_map, isColimitCoconeOfConeUnop_desc
|
coconeOpEquiv π | CompOp | 6 mathmath: coconeOpEquiv_inverse_map, coconeOpEquiv_functor_obj, coconeOpEquiv_inverse_obj, coconeOpEquiv_unitIso, coconeOpEquiv_counitIso, coconeOpEquiv_functor_map_hom
|
coconeRightOpOfCone π | CompOp | 9 mathmath: coconeRightOpOfConeEquiv_functor_map_hom, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, isLimitOfCoconeRightOpOfCone_lift, isLimitConeOfCoconeRightOp_lift, isColimitCoconeRightOpOfCone_desc, coconeRightOpOfCone_ΞΉ, coconeRightOpOfConeEquiv_counitIso, coconeRightOpOfConeEquiv_functor_obj, coconeRightOpOfCone_pt
|
coconeRightOpOfConeEquiv π | CompOp | 6 mathmath: coconeRightOpOfConeEquiv_functor_map_hom, coconeRightOpOfConeEquiv_inverse_obj, coconeRightOpOfConeEquiv_unitIso, coconeRightOpOfConeEquiv_inverse_map, coconeRightOpOfConeEquiv_counitIso, coconeRightOpOfConeEquiv_functor_obj
|
coconeUnopOfCone π | CompOp | 8 mathmath: coconeUnopOfConeEquiv_counitIso, coconeUnopOfConeEquiv_functor_obj, isLimitConeOfCoconeUnop_lift, coconeUnopOfConeEquiv_functor_map_hom, isColimitCoconeUnopOfCone_desc, coconeUnopOfCone_pt, isLimitOfCoconeUnopOfCone_lift, coconeUnopOfCone_ΞΉ
|
coconeUnopOfConeEquiv π | CompOp | 6 mathmath: coconeUnopOfConeEquiv_unitIso, coconeUnopOfConeEquiv_counitIso, coconeUnopOfConeEquiv_functor_obj, coconeUnopOfConeEquiv_functor_map_hom, coconeUnopOfConeEquiv_inverse_map, coconeUnopOfConeEquiv_inverse_obj
|
coneEquivalenceOpCoconeOp π | CompOp | β |
coneLeftOpOfCocone π | CompOp | 8 mathmath: coneLeftOpOfCocone_Ο_app, isColimitOfConeLeftOpOfCocone_desc, coneLeftOpOfCocone_pt, isLimitConeLeftOpOfCocone_lift, coneLeftOpOfCoconeEquiv_functor_map_hom, coneLeftOpOfCoconeEquiv_functor_obj, coneLeftOpOfCoconeEquiv_counitIso, isColimitCoconeOfConeLeftOp_desc
|
coneLeftOpOfCoconeEquiv π | CompOp | 6 mathmath: coneLeftOpOfCoconeEquiv_inverse_obj, coneLeftOpOfCoconeEquiv_functor_map_hom, coneLeftOpOfCoconeEquiv_functor_obj, coneLeftOpOfCoconeEquiv_unitIso, coneLeftOpOfCoconeEquiv_inverse_map, coneLeftOpOfCoconeEquiv_counitIso
|
coneOfCoconeLeftOp π | CompOp | 8 mathmath: isColimitCoconeLeftOpOfCone_desc, coconeLeftOpOfConeEquiv_inverse_obj, coneOfCoconeLeftOp_Ο_app, isColimitOfConeOfCoconeLeftOp_desc, coneOfCoconeLeftOp_pt, isLimitConeOfCoconeLeftOp_lift, coconeLeftOpOfConeEquiv_counitIso, coconeLeftOpOfConeEquiv_inverse_map
|
coneOfCoconeRightOp π | CompOp | 8 mathmath: coneOfCoconeRightOp_Ο, coconeRightOpOfConeEquiv_inverse_obj, coconeRightOpOfConeEquiv_inverse_map, isLimitConeOfCoconeRightOp_lift, coneOfCoconeRightOp_pt, isColimitCoconeRightOpOfCone_desc, coconeRightOpOfConeEquiv_counitIso, isColimitOfConeOfCoconeRightOp_desc
|
coneOfCoconeUnop π | CompOp | 8 mathmath: coconeUnopOfConeEquiv_counitIso, coneOfCoconeUnop_Ο, isLimitConeOfCoconeUnop_lift, isColimitCoconeUnopOfCone_desc, coconeUnopOfConeEquiv_inverse_map, coconeUnopOfConeEquiv_inverse_obj, isColimitOfConeOfCoconeUnop_desc, coneOfCoconeUnop_pt
|
coneOpEquiv π | CompOp | 6 mathmath: coneOpEquiv_unitIso, coneOpEquiv_inverse_obj, coneOpEquiv_functor_obj, coneOpEquiv_counitIso, coneOpEquiv_functor_map_hom, coneOpEquiv_inverse_map
|
coneRightOpOfCocone π | CompOp | 8 mathmath: isLimitConeRightOpOfCocone_lift, coneRightOpOfCoconeEquiv_functor_obj, coneRightOpOfCoconeEquiv_functor_map_hom, isColimitOfConeRightOpOfCocone_desc, coneRightOpOfCocone_Ο, coneRightOpOfCocone_pt, isColimitCoconeOfConeRightOp_desc, coneRightOpOfCoconeEquiv_counitIso
|
coneRightOpOfCoconeEquiv π | CompOp | 6 mathmath: coneRightOpOfCoconeEquiv_functor_obj, coneRightOpOfCoconeEquiv_functor_map_hom, coneRightOpOfCoconeEquiv_inverse_obj, coneRightOpOfCoconeEquiv_inverse_map, coneRightOpOfCoconeEquiv_unitIso, coneRightOpOfCoconeEquiv_counitIso
|
coneUnopOfCocone π | CompOp | 8 mathmath: coneUnopOfCoconeEquiv_counitIso, coneUnopOfCocone_pt, isColimitOfConeUnopOfCocone_desc, isLimitConeUnopOfCocone_lift, coneUnopOfCoconeEquiv_functor_map_hom, coneUnopOfCoconeEquiv_functor_obj, coneUnopOfCocone_Ο, isColimitCoconeOfConeUnop_desc
|
coneUnopOfCoconeEquiv π | CompOp | 6 mathmath: coneUnopOfCoconeEquiv_counitIso, coneUnopOfCoconeEquiv_functor_map_hom, coneUnopOfCoconeEquiv_functor_obj, coneUnopOfCoconeEquiv_inverse_obj, coneUnopOfCoconeEquiv_inverse_map, coneUnopOfCoconeEquiv_unitIso
|
inhabitedCocone π | CompOp | β |
inhabitedCoconeMorphism π | CompOp | β |
inhabitedCone π | CompOp | β |
inhabitedConeMorphism π | CompOp | β |
| Name | Category | Theorems |
category π | CompOp | 236 mathmath: CategoryTheory.Functor.LeftExtension.coconeAtFunctor_map_hom, category_id_hom, CategoryTheory.Limits.IsColimit.uniqueUpToIso_hom, CategoryTheory.Limits.coneOpEquiv_unitIso, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_map_hom, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_obj, whiskeringEquivalence_counitIso, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_map_hom, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, CategoryTheory.Limits.coneUnopOfCoconeEquiv_counitIso, CategoryTheory.WithInitial.coconeEquiv_functor_obj_pt, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ΞΉ_app, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, equivalenceOfReindexing_inverse, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom, CategoryTheory.Functor.mapCoconePrecompose_inv_hom, CategoryTheory.Limits.PushoutCocone.unop_Ο_app, CategoryTheory.Functor.mapCoconeWhisker_hom_hom, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_right, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, extendComp_inv_hom, CategoryTheory.Functor.Final.colimitCoconeOfComp_isColimit, CategoryTheory.Functor.Final.coconesEquiv_unitIso, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, CategoryTheory.Limits.coconeUnopOfConeEquiv_unitIso, extendIso_inv_hom, CategoryTheory.Limits.instIsIsoHomHomCocone, CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom, equivalenceOfReindexing_functor, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, CategoryTheory.Limits.colimit.map_desc, CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app, CategoryTheory.Functor.Final.coconesEquiv_functor, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_hom, CategoryTheory.Limits.CoconeMorphism.hom_inv_id_assoc, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_obj, functorialityEquivalence_counitIso, CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_map_hom, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_obj, extendIso_hom_hom, functorialityEquivalence_unitIso, category_comp_hom, CategoryTheory.IsUniversalColimit.precompose_isIso, CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc_assoc, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc, CategoryTheory.Limits.Cofan.ext_inv_hom, CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc, equivalenceOfReindexing_counitIso, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom, CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism, functoriality_obj_ΞΉ_app, CategoryTheory.Limits.coneOpEquiv_inverse_obj, CategoryTheory.Limits.DiagramOfCocones.coconePoints_map, CategoryTheory.WithInitial.coconeEquiv_counitIso_inv_app_hom, CategoryTheory.Limits.coconeUnopOfConeEquiv_counitIso, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_star, CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_obj, CategoryTheory.Adjunction.functorialityUnit_app_hom, cocone_iso_of_hom_iso, CategoryTheory.Limits.Multicofork.ext_hom_hom, CategoryTheory.WithInitial.coconeEquiv_unitIso_hom_app_hom_right, CategoryTheory.Functor.mapCoconeMapCocone_hom_hom, CategoryTheory.Limits.PushoutCocone.eta_inv_hom, precomposeComp_hom_app_hom, functoriality_map_hom, CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_map_hom, extendId_inv_hom, CategoryTheory.Limits.coconeOpEquiv_inverse_map, reflects_cocone_isomorphism, CategoryTheory.Limits.BinaryCofan.ext_hom_hom, whiskering_map_hom, CategoryTheory.Limits.coconeOpEquiv_functor_obj, CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom, toStructuredArrow_obj, CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_obj, CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_map, CategoryTheory.IsVanKampenColimit.precompose_isIso, CategoryTheory.WithInitial.coconeEquiv_functor_map_hom, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_hom, precomposeId_hom_app_hom, CategoryTheory.Limits.DiagramOfCocones.comp, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_left_as, CategoryTheory.Limits.Cofork.Ο_precompose, precomposeEquivalence_counitIso, equivStructuredArrow_unitIso, CategoryTheory.Limits.Cofan.ext_hom_hom, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_obj, CategoryTheory.Limits.Cowedge.ext_hom_hom, precompose_map_hom, CategoryTheory.Limits.Cocones.cone_iso_of_hom_iso, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom, fromStructuredArrow_obj_pt, CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_obj, forget_map, CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_map_hom, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom, CategoryTheory.Limits.coneOpEquiv_functor_obj, CategoryTheory.Limits.coconeRightOpOfConeEquiv_unitIso, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ΞΉ_app_right, CategoryTheory.Limits.coneOpEquiv_counitIso, CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_map_hom, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom, functorialityEquivalence_inverse, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom, CategoryTheory.Adjunction.functorialityCounit_app_hom, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_of, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_pt, CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app', precomposeId_inv_app_hom, CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_map, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_Ο, CategoryTheory.Functor.LeftExtension.coconeAtFunctor_obj, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_map, CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom, precompose_obj_ΞΉ, CategoryTheory.Limits.Multicofork.isoOfΟ_hom_hom, SheafOfModules.Presentation.map_relations_I, CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_obj, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_pt, CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_obj, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, eta_inv_hom, CategoryTheory.Limits.Cofork.ext_inv, CategoryTheory.Limits.Cocones.reflects_cone_isomorphism, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_unitIso, CategoryTheory.Limits.Cocones.functoriality_faithful, CategoryTheory.Functor.mapCoconeWhisker_inv_hom, CategoryTheory.Limits.coconeOpEquiv_inverse_obj, fromStructuredArrow_map_hom, ext_hom_hom, CategoryTheory.Limits.CoconeMorphism.hom_inv_id, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ΞΉ_app, CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc_assoc, CategoryTheory.Limits.coneOpEquiv_functor_map_hom, CategoryTheory.Limits.Cocones.functoriality_full, ext_inv_hom_hom, functoriality_obj_pt, CategoryTheory.Limits.Multicofork.ext_inv_hom, CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj, forget_obj, CategoryTheory.Limits.coconeOpEquiv_unitIso, whiskeringEquivalence_inverse, precomposeEquivalence_functor, CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, CategoryTheory.Limits.Cowedge.ext_inv_hom, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_map_hom, functorialityEquivalence_functor, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_obj, CategoryTheory.Limits.Cofork.ext_hom, equivStructuredArrow_inverse, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_unitIso, CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_map, CategoryTheory.Limits.coconeRightOpOfConeEquiv_counitIso, mapCoconeToOver_inv_hom, CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_obj, CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply, CategoryTheory.Limits.colimit.map_desc_assoc, precomposeEquivalence_unitIso, CategoryTheory.Functor.mapConeOp_inv_hom, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_Ο, CategoryTheory.Functor.Final.coconesEquiv_counitIso, CategoryTheory.Limits.IsColimit.hom_isIso, CategoryTheory.Limits.IsColimit.uniqueUpToIso_inv, CategoryTheory.Limits.coneOpEquiv_inverse_map, CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_obj, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse, CategoryTheory.Limits.CoconeMorphism.inv_hom_id, ext_inv_hom, CategoryTheory.WithInitial.coconeEquiv_counitIso_hom_app_hom, CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom, CategoryTheory.Limits.DiagramOfCocones.id, CategoryTheory.Limits.IsColimit.ofIsoColimit_desc, functoriality_faithful, whiskeringEquivalence_unitIso, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_counitIso, CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom, CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_map_hom, whiskering_obj, CategoryTheory.Functor.mapCoconePrecompose_hom_hom, CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone, equivalenceOfReindexing_unitIso, functoriality_full, extendComp_hom_hom, CategoryTheory.Functor.mapConeOp_hom_hom, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_map, toStructuredArrow_map, CategoryTheory.Limits.coconeOpEquiv_counitIso, CategoryTheory.Functor.Final.extendCocone_obj_pt, CategoryTheory.Limits.PushoutCocone.eta_hom_hom, ext_inv_inv_hom, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_counitIso, CategoryTheory.Limits.Multicofork.isoOfΟ_inv_hom, precomposeEquivalence_inverse, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso, CategoryTheory.Limits.instIsIsoHomInvCocone, CategoryTheory.Functor.Final.extendCocone_map_hom, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom, mapCoconeToOver_hom_hom, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_unitIso, CategoryTheory.Limits.CoconeMorphism.inv_hom_id_assoc, eta_hom_hom, precomposeComp_inv_app_hom, CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom, equivStructuredArrow_functor, fromStructuredArrow_obj_ΞΉ, equivStructuredArrow_counitIso, CategoryTheory.Functor.mapCoconeMapCocone_inv_hom, extendId_hom_hom, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_map, CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc, CategoryTheory.WithInitial.coconeEquiv_unitIso_inv_app_hom_right, CategoryTheory.Limits.coconeOpEquiv_functor_map_hom, instIsIsoExtendHom, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor, CategoryTheory.Functor.Final.coconesEquiv_inverse, whiskeringEquivalence_functor, CategoryTheory.Limits.coneUnopOfCoconeEquiv_unitIso, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_obj, precompose_obj_pt, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_counitIso, CategoryTheory.Functor.Final.colimitCoconeOfComp_cocone
|
equiv π | CompOp | β |
equivalenceOfReindexing π | CompOp | 6 mathmath: equivalenceOfReindexing_inverse, equivalenceOfReindexing_functor, equivalenceOfReindexing_counitIso, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_hom, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv, equivalenceOfReindexing_unitIso
|
eta π | CompOp | 3 mathmath: equivStructuredArrow_unitIso, eta_inv_hom, eta_hom_hom
|
ext π | CompOp | 9 mathmath: CategoryTheory.Functor.Final.coconesEquiv_unitIso, CategoryTheory.TransfiniteCompositionOfShape.map_isColimit, SheafOfModules.Presentation.map_relations_I, ext_hom_hom, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit, CategoryTheory.Functor.Final.coconesEquiv_counitIso, ext_inv_hom, CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isColimit, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso
|
ext_inv π | CompOp | 10 mathmath: whiskeringEquivalence_counitIso, functorialityEquivalence_counitIso, functorialityEquivalence_unitIso, equivalenceOfReindexing_counitIso, precomposeEquivalence_counitIso, ext_inv_hom_hom, precomposeEquivalence_unitIso, whiskeringEquivalence_unitIso, equivalenceOfReindexing_unitIso, ext_inv_inv_hom
|
extend π | CompOp | 17 mathmath: CategoryTheory.Limits.IndObjectPresentation.extend_ΞΉ_app_app, extendComp_inv_hom, CategoryTheory.Limits.colimit.desc_extend, CategoryTheory.Limits.IsColimit.homIso_hom, extendIso_inv_hom, extendIso_hom_hom, CategoryTheory.Limits.IsColimit.homEquiv_apply, extendId_inv_hom, CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac, extendHom_hom, CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app, extendComp_hom_hom, extend_ΞΉ, CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac, extend_pt, extendId_hom_hom, instIsIsoExtendHom
|
extendComp π | CompOp | 2 mathmath: extendComp_inv_hom, extendComp_hom_hom
|
extendHom π | CompOp | 2 mathmath: extendHom_hom, instIsIsoExtendHom
|
extendId π | CompOp | 2 mathmath: extendId_inv_hom, extendId_hom_hom
|
extendIso π | CompOp | 2 mathmath: extendIso_inv_hom, extendIso_hom_hom
|
extensions π | CompOp | 1 mathmath: extensions_app
|
forget π | CompOp | 2 mathmath: forget_map, forget_obj
|
functoriality π | CompOp | 19 mathmath: functorialityEquivalence_counitIso, functorialityEquivalence_unitIso, functoriality_obj_ΞΉ_app, CategoryTheory.Adjunction.functorialityUnit_app_hom, functoriality_map_hom, reflects_cocone_isomorphism, CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom, functorialityEquivalence_inverse, CategoryTheory.Adjunction.functorialityCounit_app_hom, CategoryTheory.Limits.Cocones.reflects_cone_isomorphism, CategoryTheory.Limits.Cocones.functoriality_faithful, CategoryTheory.Limits.Cocones.functoriality_full, functoriality_obj_pt, functorialityEquivalence_functor, CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom, functoriality_faithful, functoriality_full
|
functorialityCompFunctoriality π | CompOp | β |
functorialityEquivalence π | CompOp | 4 mathmath: functorialityEquivalence_counitIso, functorialityEquivalence_unitIso, functorialityEquivalence_inverse, functorialityEquivalence_functor
|
op π | CompOp | 21 mathmath: CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, CategoryTheory.Functor.mapCoconeOp_inv_hom, op_pt, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, CategoryTheory.Limits.coconeOpEquiv_functor_obj, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Presheaf.isSheaf_iff_isLimit, CategoryTheory.Limits.PushoutCocone.op_Ο_app, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, TopCat.Presheaf.isGluing_iff_pairwise, CategoryTheory.Functor.mapCoconeOp_hom_hom, op_Ο, CategoryTheory.Limits.coconeOpEquiv_counitIso, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, CategoryTheory.Limits.coconeOpEquiv_functor_map_hom, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
|
precompose π | CompOp | 43 mathmath: whiskeringEquivalence_counitIso, equivalenceOfReindexing_inverse, CategoryTheory.Functor.mapCoconePrecompose_inv_hom, CategoryTheory.Limits.PushoutCocone.unop_Ο_app, CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom, equivalenceOfReindexing_functor, CategoryTheory.Limits.colimit.map_desc, CategoryTheory.IsUniversalColimit.precompose_isIso, CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc_assoc, CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc, equivalenceOfReindexing_counitIso, CategoryTheory.Limits.DiagramOfCocones.coconePoints_map, precomposeComp_hom_app_hom, CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom, CategoryTheory.IsVanKampenColimit.precompose_isIso, precomposeId_hom_app_hom, CategoryTheory.Limits.DiagramOfCocones.comp, CategoryTheory.Limits.Cofork.Ο_precompose, precomposeEquivalence_counitIso, precompose_map_hom, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom, CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_map_hom, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom, precomposeId_inv_app_hom, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, precompose_obj_ΞΉ, SheafOfModules.Presentation.map_relations_I, CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc_assoc, whiskeringEquivalence_inverse, precomposeEquivalence_functor, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit, CategoryTheory.Limits.colimit.map_desc_assoc, precomposeEquivalence_unitIso, CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom, CategoryTheory.Limits.DiagramOfCocones.id, whiskeringEquivalence_unitIso, CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom, CategoryTheory.Functor.mapCoconePrecompose_hom_hom, equivalenceOfReindexing_unitIso, precomposeEquivalence_inverse, precomposeComp_inv_app_hom, CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc, precompose_obj_pt
|
precomposeComp π | CompOp | 2 mathmath: precomposeComp_hom_app_hom, precomposeComp_inv_app_hom
|
precomposeEquivalence π | CompOp | 9 mathmath: CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom, functorialityEquivalence_counitIso, functorialityEquivalence_unitIso, precomposeEquivalence_counitIso, functorialityEquivalence_inverse, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom, precomposeEquivalence_functor, precomposeEquivalence_unitIso, precomposeEquivalence_inverse
|
precomposeId π | CompOp | 2 mathmath: precomposeId_hom_app_hom, precomposeId_inv_app_hom
|
pt π | CompOp | 928 mathmath: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, TopCat.binaryCofan_isColimit_iff, SimplicialObject.Splitting.cofan_inj_ΟSummand_eq_id_assoc, category_id_hom, CategoryTheory.MorphismProperty.exists_isPushout_of_isFiltered, CategoryTheory.PreOneHypercover.forkOfIsColimit_ΞΉ_map_inj_assoc, CategoryTheory.Limits.IsColimit.isZero_pt, CategoryTheory.Monad.ForgetCreatesColimits.commuting, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ΞΉ_app_right, CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_Ο, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc, CategoryTheory.Limits.Bicone.toCocone_ΞΉ_app_mk, CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift, CategoryTheory.ShortComplex.pOpcycles_Ο_isoOpcyclesOfIsColimit_inv_assoc, CategoryTheory.Limits.Types.binaryCofan_isColimit_iff, CategoryTheory.Limits.PushoutCocone.flip_pt, CategoryTheory.Limits.Cotrident.ofCocone_ΞΉ, whisker_pt, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_inv, CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_pt, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Over.forgetCocone_pt, Profinite.Extend.cocone_pt, CategoryTheory.Limits.ReflexiveCofork.app_one_eq_Ο, CommRingCat.pushoutCocone_pt, CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimit, CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt, PartOrdEmb.Limits.cocone_pt_coe, toOver_ΞΉ_app, CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit, CategoryTheory.Functor.mapCocone_ΞΉ_app, whiskeringEquivalence_counitIso, CategoryTheory.PreOneHypercover.forkOfIsColimit_pt, CategoryTheory.Limits.colimit.cocone_ΞΉ, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_map_hom, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, CategoryTheory.Limits.coneUnopOfCoconeEquiv_counitIso, CategoryTheory.Limits.Fork.Ο_comp_hom, CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.WithInitial.coconeEquiv_functor_obj_pt, CategoryTheory.MorphismProperty.exists_hom_of_isFinitelyPresentable, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeΟOpCompShrinkYonedaObj_ΞΉ_app_assoc, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inl, CategoryTheory.Limits.PushoutCocone.mk_ΞΉ_app_zero, CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_f, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom_assoc, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_pt, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ΞΉ_app, CategoryTheory.PreOneHypercover.pβ_sigmaOfIsColimit_assoc, CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension_desc, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, CategoryTheory.Presheaf.coconeOfRepresentable_pt, whisker_ΞΉ, AlgebraicTopology.DoldKan.Ξβ.Obj.map_epi_on_summand_id_assoc, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_Q, CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_X, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_f, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom, CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ΞΉ_of_isColimit', CategoryTheory.Functor.mapCoconePrecompose_inv_hom, CategoryTheory.Limits.PushoutCocone.unop_Ο_app, RingHom.EssFiniteType.exists_eq_comp_ΞΉ_app_of_isColimit, CategoryTheory.Limits.IndObjectPresentation.extend_ΞΉ_app_app, CategoryTheory.Limits.Fork.unop_ΞΉ_app_zero, ofCotrident_ΞΉ, ModuleCat.directLimitCocone_pt_carrier, unop_Ο, CategoryTheory.Limits.Multicofork.Ο_comp_hom_assoc, SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc, CategoryTheory.Functor.mapCoconeWhisker_hom_hom, CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial, CategoryTheory.Limits.asEmptyCocone_pt, CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux, CategoryTheory.Limits.Cofork.ofCocone_ΞΉ, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_pt, CategoryTheory.Limits.MonoCoprod.binaryCofan_inl, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj, CategoryTheory.Limits.IsColimit.existsUnique, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, CategoryTheory.ObjectProperty.prop_of_isColimit_cokernelCofork, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_right, CategoryTheory.Monad.beckCoequalizer_desc, toCostructuredArrow_comp_proj, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, CategoryTheory.Limits.FormalCoproduct.ΞΉ_comp_coproductIsoCofanPt_assoc, extendComp_inv_hom, CategoryTheory.Mono.of_coproductDisjoint, CategoryTheory.Functor.Elements.coconeΟOpCompShrinkYonedaObj_pt, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift, CategoryTheory.Limits.coconeOfCoconeCurry_pt, CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom, skyscraperPresheafCocone_pt, SimplicialObject.Splitting.ΞΉ_desc_assoc, CategoryTheory.Limits.colimit.desc_extend, CategoryTheory.Limits.colimit.homIso_hom, AddCommGrpCat.isColimit_iff_bijective_desc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_pt, CategoryTheory.FinitaryExtensive.mono_ΞΉ, CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan, CategoryTheory.Functor.Final.coconesEquiv_unitIso, CategoryTheory.Limits.IsColimit.homIso_hom, toCostructuredArrow_comp_toOver_comp_forget, underPost_ΞΉ_app, CategoryTheory.IsSplitCoequalizer.asCofork_pt, CategoryTheory.Limits.Types.pUnitCocone_pt, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyΞΉ_assoc, CategoryTheory.Limits.Cotrident.Ο_eq_app_one, CategoryTheory.Limits.PushoutCocone.condition_assoc, CategoryTheory.Limits.coconeOfConeLeftOp_pt, extendIso_inv_hom, CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc, toCostructuredArrow_map, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk, CategoryTheory.Limits.IsColimit.mono_ΞΉ_app_of_isFiltered, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, CategoryTheory.Limits.PushoutCocone.op_snd, CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc, HasCardinalLT.Set.cocone_pt, CategoryTheory.Limits.instIsIsoHomHomCocone, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom, CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom, CategoryTheory.Limits.CokernelCofork.IsColimit.comp_Ο_eq_zero_iff_up_to_refinements, CategoryTheory.Limits.IsColimit.ΞΉ_map, CategoryTheory.BinaryCofan.isVanKampen_iff, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, Preorder.coconePt_mem_upperBounds, CategoryTheory.Functor.costructuredArrowMapCocone_pt, CategoryTheory.Presieve.isSheafFor_iff_preservesProduct, CategoryTheory.Limits.Multicofork.ofSigmaCofork_ΞΉ_app_right', CategoryTheory.Limits.colimit.map_desc, CategoryTheory.Limits.PullbackCone.op_pt, w_assoc, CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom, CategoryTheory.Limits.cokernel.zeroCokernelCofork_Ο, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ΞΉ, CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi, AlgebraicTopology.DoldKan.Ξβ.Obj.map_on_summand_assoc, CategoryTheory.Limits.CokernelCofork.Ο_mapOfIsColimit, CategoryTheory.Limits.coneUnopOfCocone_pt, CategoryTheory.Limits.Cofork.unop_Ο_app_one, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ΞΉ_transitionMap, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ΞΉ_app, CategoryTheory.Limits.Cofork.IsColimit.epi, CategoryTheory.Presieve.firstMap_eq_secondMap, toCostructuredArrowCompProj_hom_app, CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux, CategoryTheory.isPullback_of_cofan_isVanKampen, CategoryTheory.Limits.Types.binaryCoproductColimit_desc, CategoryTheory.Limits.opCoproductIsoProduct'_comp_self, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app, CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_hom, CategoryTheory.Limits.Cowedge.IsColimit.Ο_desc_assoc, CategoryTheory.Limits.CoconeMorphism.hom_inv_id_assoc, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom, CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_pt, CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural, CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc, CategoryTheory.Limits.BinaryBicone.toCocone_ΞΉ_app_right, HomotopicalAlgebra.AttachCells.ofArrowIso_gβ, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, CategoryTheory.Limits.Multicofork.snd_app_right_assoc, CategoryTheory.Limits.coneOfCoconeRightOp_Ο, HomologicalComplex.coconeOfHasColimitEval_pt_d, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, SSet.hornββ.desc.multicofork_pt, CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.Limits.Cofork.condition_assoc, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, CategoryTheory.Limits.Bicone.toCocone_pt, CategoryTheory.Limits.coconeOfConeUnop_pt, CategoryTheory.Limits.FormalCoproduct.cofan_inj, functorialityEquivalence_counitIso, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ΞΉ_app_bot, AlgebraicTopology.DoldKan.PInfty_on_Ξβ_splitting_summand_eq_self_assoc, CategoryTheory.is_coprod_iff_isPushout, CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimitβ, ModuleCat.HasColimit.colimitCocone_pt_isModule, CategoryTheory.Functor.mapCoconeOp_inv_hom, CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit, op_pt, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, CategoryTheory.Limits.IsColimit.ΞΉ_map_assoc, CategoryTheory.Limits.CokernelCofork.IsColimit.isIso_Ο, CategoryTheory.Limits.Cofan.IsColimit.inj_desc, CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists, CompHausLike.sigmaComparison_eq_comp_isos, CategoryTheory.Functor.coconeTypesEquiv_apply_pt, CategoryTheory.Limits.Multicofork.toSigmaCofork_pt, tensor_ΞΉ_app, CategoryTheory.ObjectProperty.isStrongGenerator_iff_exists_extremalEpi, CategoryTheory.Limits.Cotrident.ofΟ_pt, extendIso_hom_hom, functorialityEquivalence_unitIso, CategoryTheory.Limits.Multicofork.condition_assoc, CategoryTheory.ShortComplex.RightHomologyData.wΞΉ_assoc, CategoryTheory.preservesColimitIso_inv_comp_desc, category_comp_hom, CategoryTheory.Limits.IsColimit.homEquiv_apply, CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc_assoc, CategoryTheory.Limits.IsColimit.desc_self, HomotopicalAlgebra.AttachCells.cell_def, CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc, CategoryTheory.Limits.PullbackCone.op_ΞΉ_app, CategoryTheory.Limits.Cofan.ext_inv_hom, CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc, CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit, equivalenceOfReindexing_counitIso, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc_assoc, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom, CategoryTheory.Limits.Cowedge.IsColimit.Ο_desc, CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under, CategoryTheory.Limits.IsColimit.isIso_colimMap_ΞΉ, CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_f, CategoryTheory.Limits.Fork.unop_ΞΉ_app_one, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, functoriality_obj_ΞΉ_app, CategoryTheory.ObjectProperty.prop_of_isColimit_binaryCofan, CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q, CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f_assoc, PartOrdEmb.Limits.CoconePt.fac_apply, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr, toCostructuredArrowCompToOverCompForget_inv_app, CategoryTheory.Monad.beckAlgebraCofork_pt, CategoryTheory.Limits.Cowedge.condition_assoc, CategoryTheory.Limits.Cofork.app_zero_eq_comp_Ο_left, CategoryTheory.Limits.cokernel.zeroCokernelCofork_pt, CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_pt, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_H, CategoryTheory.WithInitial.coconeEquiv_counitIso_inv_app_hom, HomotopicalAlgebra.AttachCells.hm_assoc, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom, CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_f, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv_assoc, CategoryTheory.Limits.Cotrident.condition_assoc, CategoryTheory.Limits.coconeUnopOfConeEquiv_counitIso, CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer', CategoryTheory.Limits.CoconeMorphism.w_assoc, CategoryTheory.Limits.coneOfCoconeLeftOp_Ο_app, CategoryTheory.Limits.coneOfCoconeUnop_Ο, CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc, CategoryTheory.Functor.coconeTypesEquiv_symm_apply_pt, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_star, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv_assoc, CategoryTheory.Limits.FormalCoproduct.cofan_inj_Ο, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff', CategoryTheory.Under.liftCocone_ΞΉ_app, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc, CategoryTheory.Limits.Cofork.IsColimit.homIso_apply_coe, CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift, CommAlgCat.binaryCofan_pt, SSet.hornββ.desc.multicofork_Ο_two_assoc, CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc, CategoryTheory.Limits.PushoutCocone.ofCocone_ΞΉ, CategoryTheory.Adjunction.functorialityUnit_app_hom, CategoryTheory.Limits.Multicofork.ext_hom_hom, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, CategoryTheory.Pairwise.cocone_pt, CategoryTheory.Limits.Multicofork.ofSigmaCofork_Ο, CategoryTheory.WithInitial.coconeEquiv_unitIso_hom_app_hom_right, CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_fst, CategoryTheory.Limits.Concrete.isColimit_exists_rep, CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj, SSet.hornββ.desc.multicofork_Ο_zero_assoc, ModuleCat.directLimitIsColimit_desc, SSet.finite_of_isColimit, CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_inv, CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_map, CategoryTheory.Limits.Cofan.inj_injective_of_isColimit, Preorder.coconeOfUpperBound_pt, CategoryTheory.Limits.Multicofork.ofSigmaCofork_pt, ModuleCat.directLimitCocone_pt_isAddCommGroup, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom, CategoryTheory.Functor.mapCoconeMapCocone_hom_hom, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.PushoutCocone.eta_inv_hom, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk, CategoryTheory.Limits.PreservesColimitβ.map_ΞΉ_comp_isoObjConePointsOfIsColimit_hom, precomposeComp_hom_app_hom, CategoryTheory.Limits.Fork.op_pt, CategoryTheory.Limits.Multicofork.Ο_eq_app_right, functoriality_map_hom, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyΞΉ, HomologicalComplex.coconeOfHasColimitEval_pt_X, CommRingCat.FilteredColimits.nontrivial, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, SimplicialObject.Splitting.ΞΉSummand_comp_d_comp_ΟSummand_eq_zero, extendId_inv_hom, CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom_assoc, CategoryTheory.Limits.WidePushoutShape.mkCocone_pt, CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_snd, CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit, CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_pt, CategoryTheory.Limits.Cofork.op_Ο_app_zero, CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_pt, AddCommGrpCat.Colimits.colimitCocone_pt, CategoryTheory.Limits.Cofork.IsColimit.Ο_desc_assoc, CategoryTheory.Limits.BinaryCofan.ext_hom_hom, CategoryTheory.PreOneHypercover.pβ_sigmaOfIsColimit, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ΞΉ, PartOrdEmb.Limits.cocone_ΞΉ_app, CategoryTheory.Limits.pushoutCoconeOfRightIso_x, CategoryTheory.Limits.PushoutCocone.condition_zero, CategoryTheory.Functor.functorialityCompPrecompose_hom_app_hom, CategoryTheory.Limits.pointwiseCocone_pt, Condensed.isColimitLocallyConstantPresheaf_desc_apply, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, CategoryTheory.Comma.colimitAuxiliaryCocone_pt, toStructuredArrow_obj, CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc, CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_obj, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id, CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl, CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_map, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ΞΉ_app, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt, CategoryTheory.Comma.coconeOfPreserves_pt_right, CategoryTheory.TransfiniteCompositionOfShape.map_isColimit, CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre, CategoryTheory.Limits.PushoutCocone.ΞΉ_app_left, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_Ο, CategoryTheory.WithInitial.coconeEquiv_functor_map_hom, CategoryTheory.Abelian.AbelianStruct.imageΞΉ_Ο_assoc, CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_hom, CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_hom, CategoryTheory.Limits.Multicofork.map_pt, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ΞΉ_app_left, AlgebraicTopology.DoldKan.NβΞβ_inv_app_f_f, CategoryTheory.Limits.opProductIsoCoproduct'_comp_self, CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac, precomposeId_hom_app_hom, CategoryTheory.Limits.PushoutCocone.ofCocone_pt, CategoryTheory.Limits.DiagramOfCocones.comp, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_left_as, CategoryTheory.Limits.Cofork.Ο_precompose, CategoryTheory.Limits.ReflexiveCofork.condition, CategoryTheory.SmallObject.coconeOfLE_pt, precomposeEquivalence_counitIso, CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom, CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv_assoc, CategoryTheory.Limits.isLimitConeUnopOfCocone_lift, CategoryTheory.Limits.Cofan.ext_hom_hom, CategoryTheory.Limits.IndObjectPresentation.yoneda_isColimit_desc, CategoryTheory.Presheaf.tautologicalCocone'_pt, CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen, CategoryTheory.Limits.Bicone.ofColimitCocone_ΞΉ, CategoryTheory.isSheaf_pointwiseColimit, CategoryTheory.Limits.MonoCoprod.mono_of_injective, CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit, CategoryTheory.Limits.coneOfCoconeLeftOp_pt, CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr, CategoryTheory.Limits.Cowedge.ext_hom_hom, CategoryTheory.Limits.PreservesColimitβ.map_ΞΉ_comp_isoObjConePointsOfIsColimit_hom_assoc, CategoryTheory.Limits.Multicofork.ofSigmaCofork_ΞΉ_app_right, precompose_map_hom, CategoryTheory.Mono.cofanInr_of_binaryCoproductDisjoint, CategoryTheory.Limits.PushoutCocone.ΞΉ_app_right, CategoryTheory.Functor.coconeOfIsLeftKanExtension_ΞΉ, CategoryTheory.Limits.coneRightOpOfCocone_Ο, CategoryTheory.GradedObject.CofanMapObjFun.ΞΉMapObj_iso_inv, SimplicialObject.Splitting.ΟSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, SSet.hasDimensionLT_of_isColimit, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoNβ_hom_app_f_f, SimplicialObject.Splitting.cofan_inj_ΟSummand_eq_id, TopCat.isClosed_iff_of_isColimit, CategoryTheory.Comma.coconeOfPreserves_ΞΉ_app_right, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q, CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq, CategoryTheory.Limits.Cowedge.mk_pt, CategoryTheory.Mono.cofanInl_of_binaryCoproductDisjoint, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom, toOver_pt, fromStructuredArrow_obj_pt, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Comma.coconeOfPreserves_pt_hom, ofCofork_ΞΉ, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id, CategoryTheory.Presieve.isSheafFor_of_preservesProduct, AlgebraicTopology.DoldKan.Ξβ.Obj.mapMono_on_summand_id, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ΞΉ_assoc, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_map_left, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ΞΉ_app_right, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc_app, CategoryTheory.Limits.coneOpEquiv_counitIso, CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_map_hom, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom, CategoryTheory.Limits.colim.mapShortComplex_Xβ, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc_assoc, CommRingCat.coproductCocone_pt, CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc_assoc, CategoryTheory.Adjunction.functorialityCounit_app_hom, CategoryTheory.Limits.IsColimit.pullback_zero_ext, CategoryTheory.Limits.Multicofork.ofΟ_pt, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv, CategoryTheory.isSeparator_iff_of_isColimit_cofan, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_of, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_inv_assoc, CategoryTheory.Limits.BinaryCofan.ΞΉ_app_right, PrincipalSeg.cocone_pt, CategoryTheory.Limits.Fork.Ο_comp_hom_assoc, CategoryTheory.Limits.IsColimit.homEquiv_symm_naturality, CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective, CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ΞΉ, CategoryTheory.MorphismProperty.PreIndSpreads.exists_isPushout, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt, CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit_assoc, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_pt, CategoryTheory.Limits.Multicofork.map_ΞΉ_app, TopCat.coinduced_of_isColimit, toCostructuredArrowCocone_ΞΉ_app, CategoryTheory.Limits.PushoutCocone.op_Ο_app, CategoryTheory.Limits.Cofork.coequalizer_ext, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ΞΉ_transitionMap_assoc, isColimit_iff_isIso_colimMap_ΞΉ, CategoryTheory.ShortComplex.RightHomologyData.wΞΉ, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app', CategoryTheory.PreZeroHypercover.presieveβ_sigmaOfIsColimit, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w, CategoryTheory.Monad.beckCofork_pt, CategoryTheory.Limits.PushoutCocone.coequalizer_ext, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc, CategoryTheory.preservesColimitIso_inv_comp_desc_assoc, CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl, precomposeId_inv_app_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_H, CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_map, CategoryTheory.Limits.Cofork.condition, CategoryTheory.Limits.Cofork.app_zero_eq_comp_Ο_right, CategoryTheory.IsGrothendieckAbelian.mono_of_isColimit_monoOver, HomotopicalAlgebra.AttachCells.reindex_cofanβ, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top, CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_A, SimplicialObject.Splitting.cofan_inj_ΟSummand_eq_zero, AddCommGrpCat.Colimits.Quot.ΞΉ_desc, CategoryTheory.Limits.IsColimit.pullback_hom_ext, CategoryTheory.Limits.coconeOfIsSplitEpi_pt, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc, CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit, CategoryTheory.Limits.coconeOfConeRightOp_pt, CategoryTheory.Comma.coconeOfPreserves_ΞΉ_app_left, CategoryTheory.Monad.ForgetCreatesColimits.newCocone_pt, CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_ΞΉ_app, AlgebraicTopology.DoldKan.PInfty_on_Ξβ_splitting_summand_eq_self, Algebra.codRestrictEqLocusPushoutCocone.surjective_of_isEffective, CategoryTheory.Limits.Cotrident.IsColimit.homIso_symm_apply, precompose_obj_ΞΉ, CategoryTheory.extendCofan_pt, CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom_assoc, CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift, CategoryTheory.Limits.Multicofork.isoOfΟ_hom_hom, CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.exists_desc, CategoryTheory.Limits.colimit.pre_desc_assoc, CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl', SheafOfModules.Presentation.map_relations_I, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq, CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc_assoc, CategoryTheory.Limits.colimit.pre_desc, CategoryTheory.FunctorToTypes.binaryCoproductColimit_desc, CategoryTheory.Limits.pushoutCoconeOfRightIso_ΞΉ_app_left, CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone, PresheafOfModules.colimitCocone_pt, SimplicialObject.Splitting.cofan_inj_comp_app, CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible, CategoryTheory.Limits.coneOfCoconeRightOp_pt, CategoryTheory.Functor.leftAdjointObjIsDefined_of_isColimit, CategoryTheory.Limits.colimit.ΞΉ_desc_apply, CategoryTheory.Limits.IndObjectPresentation.ofCocone_I, CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc, CategoryTheory.extendCofan_ΞΉ_app, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_pt, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc, CategoryTheory.Limits.coneLeftOpOfCocone_Ο_app, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_apply_eq, CategoryTheory.Coyoneda.colimitCocone_pt, TopCat.continuous_iff_of_isColimit, CategoryTheory.Limits.Multicofork.toSigmaCofork_Ο, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq_pt, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, CategoryTheory.Limits.Types.Colimit.ΞΉ_desc_apply, w, CategoryTheory.Limits.Multicofork.IsColimit.fac_assoc, eta_inv_hom, CategoryTheory.Limits.Cofork.app_zero_eq_comp_Ο_right_assoc, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top, CategoryTheory.Limits.Cofork.ext_inv, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, CategoryTheory.Limits.colimit.ΞΉ_desc, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_pt, CategoryTheory.Limits.MonoCoprod.mono_inl_iff, CategoryTheory.Limits.Cofork.IsColimit.homIso_natural, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.Limits.CokernelCofork.Ο_mapOfIsColimit_assoc, HomotopicalAlgebra.AttachCells.reindex_cofanβ, CategoryTheory.Limits.Multicofork.fst_app_right, AddCommGrpCat.Colimits.toCocone_pt_coe, CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv, CategoryTheory.Limits.Fork.op_ΞΉ_app, Preorder.isLUB_of_isColimit, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc, CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_right, CategoryTheory.Limits.Bicone.toCocone_ΞΉ_app, fromCostructuredArrow_pt, CategoryTheory.Limits.coconeUnopOfCone_pt, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc, CategoryTheory.Limits.IndObjectPresentation.ofCocone_isColimit, CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit_assoc, CategoryTheory.Functor.coconeOfIsLeftKanExtension_pt, SSet.hornββ.desc.multicofork_Ο_zero_assoc, CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inr, CategoryTheory.Limits.PushoutCocone.mk_pt, CategoryTheory.Limits.coneRightOpOfCocone_pt, CategoryTheory.PreOneHypercover.sigmaOfIsColimit_Y, CategoryTheory.Limits.colim.map_epi', CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc_assoc, CategoryTheory.Functor.mapCoconeWhisker_inv_hom, w_apply, CategoryTheory.Functor.mapCoconeβ_pt, CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_, CategoryTheory.Limits.MonoCoprod.mono_inj, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ΞΉ_app_none, CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc, SimplicialObject.Splitting.decomposition_id, CategoryTheory.Limits.coneLeftOpOfCocone_pt, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, ext_hom_hom, CategoryTheory.Limits.CoconeMorphism.hom_inv_id, CategoryTheory.Limits.FintypeCat.finite_of_isColimit, CategoryTheory.Limits.Fork.op_ΞΉ_app_one, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_f, CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f, CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ΞΉ_app, CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc_assoc, CategoryTheory.Presheaf.coconeOfRepresentable_naturality, CategoryTheory.ShortComplex.pOpcycles_Ο_isoOpcyclesOfIsColimit_inv, toCostructuredArrowCompToOverCompForget_hom_app, CategoryTheory.Functor.mapCoconeβ_ΞΉ_app, CategoryTheory.Limits.Cofork.unop_Ο_app_zero, CategoryTheory.Limits.ReflexiveCofork.mk_pt, CategoryTheory.Limits.IsColimit.hom_desc, CategoryTheory.Functor.Final.colimit_cocone_comp_aux, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CategoryTheory.FunctorToTypes.jointly_surjective, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ΞΉ, CategoryTheory.Limits.Cofork.IsColimit.existsUnique, CategoryTheory.Limits.combineCocones_pt_obj, Algebra.codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul, CommRingCat.coproductCoconeIsColimit_desc, CategoryTheory.Limits.Cotrident.app_one, CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeΟOpCompShrinkYonedaObj_ΞΉ_app, CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi, ext_inv_hom_hom, CategoryTheory.Abelian.AbelianStruct.imageΞΉ_Ο, CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_pt, functoriality_obj_pt, CategoryTheory.Limits.CokernelCofork.condition_assoc, CategoryTheory.Limits.Multicofork.ext_inv_hom, AlgebraicTopology.DoldKan.Ξβ.Obj.map_on_summand, CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift, CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj, SSet.iSup_range_eq_top_of_isColimit, AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_pt, CategoryTheory.GradedObject.CofanMapObjFun.ΞΉMapObj_iso_inv_assoc, CategoryTheory.Limits.CoproductDisjoint.nonempty_isInitial_of_ne, ModuleCat.FilteredColimits.ΞΉ_colimitDesc, CategoryTheory.Limits.colimit.existsUnique, CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr', ofPushoutCocone_ΞΉ, forget_obj, SSet.hornββ.desc.multicofork_Ο_three_assoc, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv_assoc, CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift, CategoryTheory.ObjectProperty.prop_of_isColimit_cofan, CategoryTheory.Limits.Cotrident.coequalizer_ext, CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app, CategoryTheory.Limits.IndObjectPresentation.ofCocone_ΞΉ, CategoryTheory.ObjectProperty.prop_of_isColimit, CategoryTheory.Limits.colimit.ΞΉ_coconeMorphism, CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff, CategoryTheory.Limits.Cowedge.ext_inv_hom, CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_map, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, CategoryTheory.Limits.CokernelCofork.map_condition, CategoryTheory.Limits.CoproductDisjoint.mono_inj, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.PreservesColimitβ.ΞΉ_comp_isoObjConePointsOfIsColimit_inv, CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc, LightProfinite.Extend.cocone_pt, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_map_hom, CategoryTheory.Limits.colimit.ΞΉ_desc_assoc, CategoryTheory.IsPushout.of_is_coproduct, CategoryTheory.Abelian.mono_inl_of_isColimit, CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj_assoc, CategoryTheory.Limits.Cofork.ext_hom, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone_pt, CategoryTheory.Limits.colimit.ΞΉ_desc_app_assoc, toCostructuredArrow_obj, CategoryTheory.Under.liftCocone_pt, CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right, CategoryTheory.Limits.coconePointwiseProduct_pt, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ΞΉ_assoc, CategoryTheory.Preadditive.epi_iff_isZero_cokernel', CategoryTheory.Limits.Types.jointly_surjective, CategoryTheory.Limits.CokernelCofork.map_Ο, CategoryTheory.Over.liftCocone_ΞΉ_app, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm, CategoryTheory.Limits.PullbackCone.unop_pt, CategoryTheory.Limits.coconeRightOpOfConeEquiv_counitIso, SimplicialObject.Splitting.ΞΉ_desc, mapCoconeToOver_inv_hom, CategoryTheory.Limits.wideCoequalizer.cotrident_ΞΉ_app_one, CategoryTheory.Limits.IndObjectPresentation.ofCocone_F, CategoryTheory.Limits.Cofan.cofanTypes_pt, CategoryTheory.Limits.IsColimit.ΞΉ_smul, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map, CategoryTheory.Functor.LeftExtension.coconeAt_pt, SimplicialObject.Splitting.ΟSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, CategoryTheory.Limits.colim.mapShortComplex_Xβ, CategoryTheory.Limits.IndObjectPresentation.ofCocone_β, CategoryTheory.Limits.pushoutCoconeOfLeftIso_x, CategoryTheory.Limits.BinaryCofan.ΞΉ_app_left, CategoryTheory.Limits.colimit.map_desc_assoc, CategoryTheory.Limits.BinaryBicone.toCocone_ΞΉ_app_left, ModuleCat.HasColimit.colimitCocone_pt_carrier, CategoryTheory.Limits.PushoutCocone.op_pt, CategoryTheory.Limits.PushoutCocone.mk_ΞΉ_app_right, CategoryTheory.Limits.Multicofork.snd_app_right, precomposeEquivalence_unitIso, CategoryTheory.Limits.Cotrident.condition, HomotopicalAlgebra.AttachCells.cell_def_assoc, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f, CategoryTheory.Functor.Final.coconesEquiv_counitIso, CategoryTheory.SmallObject.SuccStruct.iterationCocone_pt, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_hom_assoc, CategoryTheory.isCardinalPresentable_of_isColimit', CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer', CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe, CategoryTheory.Limits.combineCocones_ΞΉ_app_app, CategoryTheory.Limits.DiagramOfCocones.coconePoints_obj, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, CategoryTheory.Limits.coneOpEquiv_inverse_map, CategoryTheory.Limits.Types.binaryCoproductCocone_pt, CategoryTheory.Limits.Multicofork.sigma_condition, CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_A, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_ΞΉ, CategoryTheory.Limits.colimit.cocone_x, TopCat.nonempty_isColimit_iff_eq_coinduced, SimplicialObject.Splitting.cofan_inj_ΟSummand_eq_zero_assoc, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingPropertyFixedBot_ΞΉ_app_bot, CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc, CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ΞΉ_app_f, CategoryTheory.Limits.CoconeMorphism.inv_hom_id, CategoryTheory.Limits.Cone.unop_pt, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w_assoc, CategoryTheory.Functor.mapCoconeOp_hom_hom, CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer', CategoryTheory.Presieve.piComparison_fac, ext_inv_hom, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_pt, CategoryTheory.WithInitial.coconeEquiv_counitIso_hom_app_hom, AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv, TopCat.coconeOfCoconeForget_pt, AlgebraicGeometry.ofArrows_ΞΉ_mem_zariskiTopology_of_isColimit, CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom, CategoryTheory.Limits.DiagramOfCocones.id, CompleteLattice.MulticoequalizerDiagram.multicofork_pt, CategoryTheory.Limits.Multicofork.condition, CategoryTheory.Limits.IsColimit.ofIsoColimit_desc, CategoryTheory.Limits.CoconeMorphism.map_w_assoc, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, CategoryTheory.MorphismProperty.colimitsOfShape.mk', CategoryTheory.Limits.IsColimit.isIso_ΞΉ_app_of_isTerminal, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj, whiskeringEquivalence_unitIso, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv, op_Ο, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_counitIso, CategoryTheory.Limits.colimitCoconeOfUnique_cocone_pt, HomotopicalAlgebra.AttachCells.isPushout, CategoryTheory.Limits.epi_of_isColimit_parallelFamily, CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom, CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_map_hom, CategoryTheory.Limits.coconeOfCoconeUncurry_pt, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.FintypeCat.jointly_surjective, CategoryTheory.Limits.Fork.op_ΞΉ_app_zero, CategoryTheory.Limits.coconeOfCoconeUncurry_ΞΉ_app, CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr, CategoryTheory.Limits.pushoutCoconeOfRightIso_ΞΉ_app_none, CategoryTheory.Limits.colimit.post_desc, CategoryTheory.Limits.PushoutCocone.mk_ΞΉ_app_left, CategoryTheory.mono_of_cofan_isVanKampen, CategoryTheory.Functor.mapCoconePrecompose_hom_hom, SSet.hornββ.desc.multicofork_pt, CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ΞΉ_app, CategoryTheory.Limits.Cofork.op_Ο_app_one, equivalenceOfReindexing_unitIso, CategoryTheory.Limits.IsColimit.ΞΉ_app_homEquiv_symm_assoc, CategoryTheory.Limits.Bicone.ofColimitCocone_pt, CategoryTheory.Limits.Cofork.IsColimit.Ο_desc, CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift, TopCat.isOpen_iff_of_isColimit_cofork, CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_Ο, extendComp_hom_hom, toCostructuredArrowCompProj_inv_app, TopCat.isQuotientMap_of_isColimit_cofork, CategoryTheory.epi_iff_isIso_inl, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, CategoryTheory.Sheaf.sheafifyCocone_ΞΉ_app_val_assoc, extend_ΞΉ, toStructuredArrow_map, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, CategoryTheory.Limits.coconeOpEquiv_counitIso, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv, TopCat.isOpen_iff_of_isColimit, CategoryTheory.Limits.IndObjectPresentation.cocone_pt, CategoryTheory.Functor.Final.extendCocone_obj_pt, CategoryTheory.ShortComplex.Ο_isoOpcyclesOfIsColimit_hom_assoc, CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom, CategoryTheory.Limits.colim.map_mono', CategoryTheory.Limits.Multicofork.sigma_condition_assoc, CategoryTheory.Limits.Multicoequalizer.multicofork_ΞΉ_app_right, CategoryTheory.Limits.Multicofork.IsColimit.isPushout, CategoryTheory.Limits.PushoutCocone.unop_pt, CategoryTheory.Limits.PushoutCocone.eta_hom_hom, CategoryTheory.Comma.coconeOfPreserves_pt_left, ext_inv_inv_hom, CategoryTheory.isCardinalPresentable_of_isColimit, CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc, AlgebraicTopology.DoldKan.Ξβ.Obj.mapMono_on_summand_id_assoc, CategoryTheory.Limits.Cofork.ofΟ_pt, CategoryTheory.Limits.coconeOfDiagramInitial_pt, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_counitIso, CategoryTheory.Limits.BinaryBicone.toCocone_pt, TopCat.sigmaCofan_pt, CategoryTheory.Limits.Cone.op_pt, CategoryTheory.ShortComplex.exact_iff_of_forks, CategoryTheory.Limits.coequalizer.cofork_ΞΉ_app_one, CategoryTheory.Limits.Cofan.IsColimit.fac_assoc, CategoryTheory.Limits.coconeRightOpOfCone_pt, CategoryTheory.Limits.Multicofork.isoOfΟ_inv_hom, CategoryTheory.Limits.combineCocones_pt_map, toCostructuredArrowCocone_pt, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_pt, CategoryTheory.Monad.MonadicityInternal.counitCofork_pt, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ΞΉ_app_eq_sum, CategoryTheory.Limits.FormalCoproduct.ΞΉ_comp_coproductIsoCofanPt, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso, CategoryTheory.Limits.CokernelCofork.map_condition_assoc, CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left, CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization, CategoryTheory.Abelian.mono_inr_of_isColimit, skyscraperPresheafCoconeOfSpecializes_pt, CategoryTheory.Limits.IsColimit.ΞΉ_app_homEquiv_symm, CategoryTheory.Limits.Cofan.IsColimit.fac, CategoryTheory.Limits.Cofork.IsColimit.homIso_symm_apply, CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc, CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.condition, CategoryTheory.Limits.Cofork.IsColimit.Ο_desc', unop_pt, CategoryTheory.Limits.CokernelCofork.Ο_eq_zero, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, CategoryTheory.Limits.instIsIsoHomInvCocone, CategoryTheory.Functor.Final.extendCocone_map_hom, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc, CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self, CategoryTheory.IsPushout.of_isColimit, CategoryTheory.Functor.mapCocone_pt, CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl, ModuleCat.directLimitCocone_pt_isModule, CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj_assoc, CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ΞΉ_of_isColimit, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_fac, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom, mapCoconeToOver_hom_hom, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, AlgebraicTopology.DoldKan.Ξβ.Obj.map_epi_on_summand_id, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, CategoryTheory.Limits.Cofork.unop_ΞΉ, CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj_assoc, CategoryTheory.preserves_desc_mapCocone, CategoryTheory.Limits.Multicofork.Ο_comp_hom, ofPushoutCocone_pt, CategoryTheory.Limits.CoconeMorphism.inv_hom_id_assoc, ModuleCat.FilteredColimits.ΞΉ_colimitDesc_assoc, CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi, CategoryTheory.Limits.CompleteLattice.colimitCocone_isColimit_desc, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc, SimplicialObject.Splitting.toKaroubiNondegComplexIsoNβ_hom_f_f, AlgebraicTopology.DoldKan.Ξβ.Obj.map_on_summand', eta_hom_hom, CategoryTheory.Limits.coneUnopOfCocone_Ο, CategoryTheory.Limits.Cotrident.app_one_assoc, CategoryTheory.Limits.Multicofork.ofSigmaCofork_ΞΉ_app_left, extend_pt, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map, CategoryTheory.Limits.coconeOfDiagramTerminal_pt, CategoryTheory.Limits.coconeOfCoconeCurry_ΞΉ_app, CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app, CategoryTheory.isSeparator_of_isColimit_cofan, precomposeComp_inv_app_hom, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.FinitaryExtensive.isPullback_initial_to, CategoryTheory.Limits.PreservesColimitβ.ΞΉ_comp_isoObjConePointsOfIsColimit_inv_assoc, SSet.hornββ.desc.multicofork_Ο_three_assoc, CategoryTheory.PreOneHypercover.forkOfIsColimit_ΞΉ_map_inj, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_ΞΉ_app_f, SSet.hornββ.desc.multicofork_Ο_one_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc, CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom, CategoryTheory.Limits.Cofork.IsColimit.Ο_desc'_assoc, CategoryTheory.Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit, CategoryTheory.Limits.IsColimit.fac_assoc, AlgebraicGeometry.SheafedSpace.isColimit_exists_rep, CategoryTheory.PreOneHypercover.pβ_sigmaOfIsColimit, CategoryTheory.Limits.pushoutCoconeOfRightIso_ΞΉ_app_right, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux, CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_Ο, SimplicialObject.Split.cofan_inj_naturality_symm, CategoryTheory.Presheaf.tautologicalCocone_pt, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, CategoryTheory.Limits.colimit.toOver_pt, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_hom, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff', SimplicialObject.Splitting.cofan_inj_comp_app_assoc, CategoryTheory.Limits.colim.mapShortComplex_Xβ, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_Ο, HomotopicalAlgebra.AttachCells.ofArrowIso_gβ, CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_obj, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ΞΉ, tensor_pt, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Functor.mapCoconeMapCocone_inv_hom, TopCat.coconeOfCoconeForget_ΞΉ_app, CategoryTheory.Comma.colimitAuxiliaryCocone_ΞΉ_app, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.wβ, CategoryTheory.Sheaf.sheafifyCocone_ΞΉ_app_val, extendId_hom_hom, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, CategoryTheory.Limits.PushoutCocone.unop_snd, CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_obj, CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit, CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_map, CategoryTheory.Limits.Cofork.app_one_eq_Ο, CategoryTheory.PreOneHypercover.pβ_sigmaOfIsColimit_assoc, CategoryTheory.ShortComplex.Ο_isoOpcyclesOfIsColimit_hom, CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc, CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ΞΉ_app, CategoryTheory.Limits.Sigma.cocone_pt, CategoryTheory.epi_iff_isIso_inr, CategoryTheory.WithInitial.coconeEquiv_unitIso_inv_app_hom_right, CategoryTheory.Limits.coconeOpEquiv_functor_map_hom, SimplicialObject.Splitting.cofan_inj_eq_assoc, CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f, underPost_pt, CategoryTheory.Limits.Cofork.op_ΞΉ, extensions_app, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.wβ_assoc, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor, CategoryTheory.Limits.Cotrident.IsColimit.homIso_apply_coe, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ΞΉ_assoc, CategoryTheory.Limits.coneOfCoconeUnop_pt, AlgebraicTopology.DoldKan.Ξβ.Obj.map_on_summand'_assoc, CategoryTheory.Limits.colimit.pre_eq, CategoryTheory.IsPushout.isVanKampen_inl, CategoryTheory.Limits.CoconeMorphism.map_w, CategoryTheory.Limits.Multicofork.IsColimit.fac, CategoryTheory.Over.liftCocone_pt, CategoryTheory.Limits.constCocone_pt, AlgebraicGeometry.PresheafedSpace.colimitCocone_pt, CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen, CategoryTheory.Limits.colimit.ΞΉ_desc_app, CategoryTheory.Limits.PushoutCocone.unop_fst, precompose_obj_pt, CategoryTheory.IsPushout.of_isColimit_cocone, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, SimplicialObject.Splitting.cofan_inj_epi_naturality, CategoryTheory.Limits.PushoutCocone.op_fst, CategoryTheory.Limits.isCokernelEpiComp_desc, CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi, CategoryTheory.Limits.Types.pushoutCocone_inr_injective_of_isColimit, CategoryTheory.Limits.Cowedge.condition, SSet.range_eq_iSup_of_isColimit, Algebra.codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_counitIso, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc, CategoryTheory.Preadditive.coforkOfCokernelCofork_pt, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst, CategoryTheory.Limits.coconeLeftOpOfCone_pt, HomotopicalAlgebra.AttachCells.hm, CategoryTheory.Limits.MonoCoprod.binaryCofan_inr, CategoryTheory.Limits.Types.Pushout.cocone_pt, CategoryTheory.Limits.epi_of_isColimit_cofork, CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_pt, CategoryTheory.Monad.ForgetCreatesColimits.newCocone_ΞΉ
|
unop π | CompOp | 5 mathmath: unop_Ο, CategoryTheory.Limits.coneOpEquiv_inverse_obj, CategoryTheory.Limits.coneOpEquiv_counitIso, CategoryTheory.Limits.coneOpEquiv_inverse_map, unop_pt
|
whisker π | CompOp | 22 mathmath: CategoryTheory.Functor.Final.colimitCoconeComp_cocone, whisker_pt, whisker_ΞΉ, CategoryTheory.Limits.PushoutCocone.unop_Ο_app, CategoryTheory.Functor.mapCoconeWhisker_hom_hom, CategoryTheory.Functor.Final.colimitCoconeComp_isColimit, CategoryTheory.Limits.PullbackCone.op_ΞΉ_app, equivalenceOfReindexing_counitIso, whiskering_map_hom, CategoryTheory.IsUniversalColimit.whiskerEquivalence, CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_ΞΉ_app, CategoryTheory.Limits.colimit.pre_desc_assoc, CategoryTheory.Limits.colimit.pre_desc, CategoryTheory.IsVanKampenColimit.whiskerEquivalence, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, CategoryTheory.Limits.Fork.op_ΞΉ_app, CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff, CategoryTheory.Functor.mapCoconeWhisker_inv_hom, whiskering_obj, equivalenceOfReindexing_unitIso, CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff, CategoryTheory.Limits.colimit.pre_eq
|
whiskering π | CompOp | 13 mathmath: whiskeringEquivalence_counitIso, equivalenceOfReindexing_inverse, CategoryTheory.Functor.Final.coconesEquiv_unitIso, equivalenceOfReindexing_functor, equivalenceOfReindexing_counitIso, whiskering_map_hom, whiskeringEquivalence_inverse, CategoryTheory.Functor.Final.coconesEquiv_counitIso, whiskeringEquivalence_unitIso, whiskering_obj, equivalenceOfReindexing_unitIso, CategoryTheory.Functor.Final.coconesEquiv_inverse, whiskeringEquivalence_functor
|
whiskeringEquivalence π | CompOp | 4 mathmath: whiskeringEquivalence_counitIso, whiskeringEquivalence_inverse, whiskeringEquivalence_unitIso, whiskeringEquivalence_functor
|
ΞΉ π | CompOp | 335 mathmath: CategoryTheory.MorphismProperty.exists_isPushout_of_isFiltered, CategoryTheory.Monad.ForgetCreatesColimits.commuting, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ΞΉ_app_right, CategoryTheory.Limits.Bicone.toCocone_ΞΉ_app_mk, CategoryTheory.Limits.Cotrident.ofCocone_ΞΉ, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_inv, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Cone.unop_ΞΉ, CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_ΞΉ_app, CategoryTheory.Limits.ReflexiveCofork.app_one_eq_Ο, toOver_ΞΉ_app, CategoryTheory.Limits.Multicofork.ofΟ_ΞΉ_app, CategoryTheory.Functor.mapCocone_ΞΉ_app, CategoryTheory.Limits.colimit.cocone_ΞΉ, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.MorphismProperty.exists_hom_of_isFinitelyPresentable, CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeΟOpCompShrinkYonedaObj_ΞΉ_app_assoc, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inl, CategoryTheory.Limits.PushoutCocone.mk_ΞΉ_app_zero, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom_assoc, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ΞΉ_app, CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension_desc, whisker_ΞΉ, CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ΞΉ_of_isColimit', CategoryTheory.Limits.PushoutCocone.unop_Ο_app, RingHom.EssFiniteType.exists_eq_comp_ΞΉ_app_of_isColimit, CategoryTheory.Limits.IndObjectPresentation.extend_ΞΉ_app_app, CategoryTheory.Limits.Fork.unop_ΞΉ_app_zero, ofCotrident_ΞΉ, unop_Ο, CategoryTheory.Limits.Cofork.ofCocone_ΞΉ, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift, CategoryTheory.Limits.colimit.homIso_hom, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, CategoryTheory.FinitaryExtensive.mono_ΞΉ, CategoryTheory.Limits.IsColimit.homIso_hom, underPost_ΞΉ_app, CategoryTheory.Limits.Cotrident.Ο_eq_app_one, toCostructuredArrow_map, CategoryTheory.Limits.Types.pUnitCocone_ΞΉ_app, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk, CategoryTheory.Limits.IsColimit.mono_ΞΉ_app_of_isFiltered, CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom, LightProfinite.Extend.cocone_ΞΉ_app, CategoryTheory.Limits.IsColimit.ΞΉ_map, CategoryTheory.Limits.Types.binaryCoproductCocone_ΞΉ_app, w_assoc, ModuleCat.HasColimit.colimitCocone_ΞΉ_app, CategoryTheory.Limits.Cofork.unop_Ο_app_one, AddCommGrpCat.Colimits.colimitCocone_ΞΉ_app, TopCat.sigmaCofan_ΞΉ_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ΞΉ_transitionMap, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ΞΉ_app, fromCostructuredArrow_ΞΉ_app, CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app, CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_ΞΉ_app, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_hom, CategoryTheory.Limits.BinaryBicone.toCocone_ΞΉ_app_right, CategoryTheory.Limits.colimit.toOver_ΞΉ_app, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, CategoryTheory.Limits.Multicofork.snd_app_right_assoc, CategoryTheory.Limits.coneOfCoconeRightOp_Ο, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ΞΉ_app_bot, CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimitβ, CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, CategoryTheory.Limits.IsColimit.ΞΉ_map_assoc, CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists, tensor_ΞΉ_app, CategoryTheory.Limits.IsColimit.homEquiv_apply, AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_ΞΉ, CategoryTheory.Limits.PullbackCone.op_ΞΉ_app, CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under, CategoryTheory.Limits.IsColimit.isIso_colimMap_ΞΉ, CategoryTheory.Limits.Fork.unop_ΞΉ_app_one, CategoryTheory.Limits.pointwiseCocone_ΞΉ_app_app, functoriality_obj_ΞΉ_app, PartOrdEmb.Limits.CoconePt.fac_apply, CategoryTheory.Limits.Cofork.app_zero_eq_comp_Ο_left, CategoryTheory.Coyoneda.colimitCocone_ΞΉ_app, AlgebraicGeometry.PresheafedSpace.colimitCocone_ΞΉ_app_base, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv_assoc, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ΞΉ_app, CategoryTheory.Limits.CoconeMorphism.w_assoc, CategoryTheory.Limits.coneOfCoconeLeftOp_Ο_app, CategoryTheory.Limits.coneOfCoconeUnop_Ο, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_star, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv_assoc, CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_ΞΉ_app, CategoryTheory.Under.liftCocone_ΞΉ_app, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc, CategoryTheory.Limits.PushoutCocone.ofCocone_ΞΉ, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ΞΉ_app, PrincipalSeg.cocone_ΞΉ_app, CategoryTheory.Limits.Concrete.isColimit_exists_rep, ModuleCat.directLimitIsColimit_desc, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk, CategoryTheory.Limits.PreservesColimitβ.map_ΞΉ_comp_isoObjConePointsOfIsColimit_hom, CategoryTheory.Limits.Multicofork.Ο_eq_app_right, functoriality_map_hom, CategoryTheory.Limits.coconePointwiseProduct_ΞΉ_app, CategoryTheory.Limits.Cofork.op_Ο_app_zero, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ΞΉ, PartOrdEmb.Limits.cocone_ΞΉ_app, CategoryTheory.Limits.PushoutCocone.condition_zero, Condensed.isColimitLocallyConstantPresheaf_desc_apply, toStructuredArrow_obj, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ΞΉ_app, CategoryTheory.Limits.PushoutCocone.ΞΉ_app_left, CategoryTheory.WithInitial.coconeEquiv_functor_map_hom, CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ΞΉ_app_left, CategoryTheory.Limits.IndObjectPresentation.yoneda_isColimit_desc, CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen, CategoryTheory.Limits.Bicone.ofColimitCocone_ΞΉ, CategoryTheory.Limits.Cofan.mk_ΞΉ_app, CategoryTheory.Limits.PushoutCocone.mk_ΞΉ_app, CategoryTheory.Limits.PreservesColimitβ.map_ΞΉ_comp_isoObjConePointsOfIsColimit_hom_assoc, precompose_map_hom, CategoryTheory.Limits.PushoutCocone.ΞΉ_app_right, CategoryTheory.Functor.coconeOfIsLeftKanExtension_ΞΉ, CategoryTheory.Limits.coneRightOpOfCocone_Ο, TopCat.isClosed_iff_of_isColimit, CategoryTheory.Comma.coconeOfPreserves_ΞΉ_app_right, CategoryTheory.Limits.coconeOfConeRightOp_ΞΉ, ofCofork_ΞΉ, CategoryTheory.Pairwise.cocone_ΞΉ_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ΞΉ_assoc, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ΞΉ_app_right, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ΞΉ_app_of, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_inv_assoc, CategoryTheory.Limits.BinaryCofan.ΞΉ_app_right, CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective, CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ΞΉ, CategoryTheory.MorphismProperty.PreIndSpreads.exists_isPushout, CategoryTheory.Limits.Multicofork.map_ΞΉ_app, TopCat.coinduced_of_isColimit, toCostructuredArrowCocone_ΞΉ_app, CategoryTheory.Limits.PushoutCocone.op_Ο_app, CategoryTheory.Limits.Cofork.coequalizer_ext, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ΞΉ_transitionMap_assoc, isColimit_iff_isIso_colimMap_ΞΉ, CategoryTheory.Functor.Final.extendCocone_obj_ΞΉ_app', CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w, CategoryTheory.Limits.PushoutCocone.coequalizer_ext, CategoryTheory.Limits.Cofork.app_zero_eq_comp_Ο_right, CategoryTheory.Limits.PullbackCone.unop_ΞΉ_app, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top, AddCommGrpCat.Colimits.toCocone_ΞΉ_app, CategoryTheory.Limits.coconeOfDiagramTerminal_ΞΉ_app, AddCommGrpCat.Colimits.Quot.ΞΉ_desc, Preorder.coconeOfUpperBound_ΞΉ_app, CategoryTheory.Limits.asEmptyCocone_ΞΉ_app, skyscraperPresheafCocone_ΞΉ_app, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_hom, CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit, CategoryTheory.Comma.coconeOfPreserves_ΞΉ_app_left, CategoryTheory.Limits.coconeOfDiagramInitial_ΞΉ_app, CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_ΞΉ_app, precompose_obj_ΞΉ, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq, CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc, CategoryTheory.Limits.pushoutCoconeOfRightIso_ΞΉ_app_left, CategoryTheory.Limits.colimit.ΞΉ_desc_apply, CategoryTheory.extendCofan_ΞΉ_app, CategoryTheory.Limits.coneLeftOpOfCocone_Ο_app, TopCat.continuous_iff_of_isColimit, CategoryTheory.Limits.Types.Colimit.ΞΉ_desc_apply, w, eta_inv_hom, CategoryTheory.Limits.Cofork.app_zero_eq_comp_Ο_right_assoc, CategoryTheory.Limits.WidePushoutShape.mkCocone_ΞΉ_app, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top, CategoryTheory.Limits.colimit.ΞΉ_desc, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.Limits.Multicofork.fst_app_right, CategoryTheory.Limits.Fork.op_ΞΉ_app, CategoryTheory.Limits.Bicone.toCocone_ΞΉ_app, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inr, CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeΞΉIteration_incl, CategoryTheory.Functor.coconeTypesEquiv_apply_ΞΉ_app, w_apply, CategoryTheory.Limits.pushoutCoconeOfLeftIso_ΞΉ_app_none, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, HasCardinalLT.Set.cocone_ΞΉ_app, CategoryTheory.Limits.Fork.op_ΞΉ_app_one, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ΞΉ_app, CategoryTheory.Presheaf.coconeOfRepresentable_naturality, CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ΞΉ_app, CategoryTheory.Functor.mapCoconeβ_ΞΉ_app, CategoryTheory.Limits.Cofork.unop_Ο_app_zero, CategoryTheory.Limits.IsColimit.hom_desc, CategoryTheory.Functor.Final.colimit_cocone_comp_aux, CategoryTheory.FunctorToTypes.jointly_surjective, HomologicalComplex.coconeOfHasColimitEval_ΞΉ_app_f, CategoryTheory.Limits.Cotrident.app_one, CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeΟOpCompShrinkYonedaObj_ΞΉ_app, SSet.iSup_range_eq_top_of_isColimit, ModuleCat.FilteredColimits.ΞΉ_colimitDesc, ofPushoutCocone_ΞΉ, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv_assoc, CategoryTheory.Limits.Cotrident.coequalizer_ext, CategoryTheory.Limits.IndObjectPresentation.ofCocone_ΞΉ, CategoryTheory.Limits.colimit.ΞΉ_coconeMorphism, CategoryTheory.Monad.beckAlgebraCofork_ΞΉ_app, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.coconeLeftOpOfCone_ΞΉ_app, CategoryTheory.Limits.PreservesColimitβ.ΞΉ_comp_isoObjConePointsOfIsColimit_inv, CategoryTheory.Limits.colimit.ΞΉ_desc_assoc, CategoryTheory.Limits.coconeRightOpOfCone_ΞΉ, CategoryTheory.Limits.colimit.ΞΉ_desc_app_assoc, toCostructuredArrow_obj, CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.Types.jointly_surjective, CategoryTheory.Over.liftCocone_ΞΉ_app, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ΞΉ_app, CategoryTheory.Limits.wideCoequalizer.cotrident_ΞΉ_app_one, ModuleCat.directLimitCocone_ΞΉ_app, CategoryTheory.Limits.IsColimit.ΞΉ_smul, Profinite.Extend.cocone_ΞΉ_app, CategoryTheory.Limits.BinaryCofan.ΞΉ_app_left, CategoryTheory.Limits.BinaryBicone.toCocone_ΞΉ_app_left, CategoryTheory.Limits.PushoutCocone.mk_ΞΉ_app_right, CategoryTheory.Limits.Multicofork.snd_app_right, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_hom_assoc, CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation, CategoryTheory.Limits.combineCocones_ΞΉ_app_app, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, TopCat.nonempty_isColimit_iff_eq_coinduced, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingPropertyFixedBot_ΞΉ_app_bot, CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ΞΉ_app_f, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w_assoc, CategoryTheory.FunctorToTypes.binaryCoproductCocone_ΞΉ_app, CategoryTheory.Limits.Sigma.cocone_ΞΉ, AlgebraicGeometry.ofArrows_ΞΉ_mem_zariskiTopology_of_isColimit, CategoryTheory.Limits.CoconeMorphism.map_w_assoc, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, CategoryTheory.Limits.IsColimit.isIso_ΞΉ_app_of_isTerminal, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj, CategoryTheory.Limits.coconeOfConeLeftOp_ΞΉ_app, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ΞΉ_app, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv, op_Ο, CategoryTheory.Limits.coconeOfConeUnop_ΞΉ, CategoryTheory.Limits.epi_of_isColimit_parallelFamily, CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.FintypeCat.jointly_surjective, CategoryTheory.Limits.Fork.op_ΞΉ_app_zero, CategoryTheory.Limits.coconeOfCoconeUncurry_ΞΉ_app, CategoryTheory.Limits.pushoutCoconeOfRightIso_ΞΉ_app_none, CategoryTheory.Presheaf.tautologicalCocone_ΞΉ_app, CategoryTheory.Presheaf.tautologicalCocone'_ΞΉ_app, CategoryTheory.Limits.PushoutCocone.mk_ΞΉ_app_left, CategoryTheory.mono_of_cofan_isVanKampen, CategoryTheory.Presheaf.coconeOfRepresentable_ΞΉ_app, CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ΞΉ_app, CategoryTheory.Limits.Cofork.op_Ο_app_one, CategoryTheory.Limits.IsColimit.ΞΉ_app_homEquiv_symm_assoc, skyscraperPresheafCoconeOfSpecializes_ΞΉ_app, CategoryTheory.Functor.Elements.coconeΟOpCompShrinkYonedaObj_ΞΉ_app, CategoryTheory.Limits.Types.Pushout.cocone_ΞΉ_app, CategoryTheory.Over.forgetCocone_ΞΉ_app, CategoryTheory.Sheaf.sheafifyCocone_ΞΉ_app_val_assoc, extend_ΞΉ, toStructuredArrow_map, TopCat.isOpen_iff_of_isColimit, CategoryTheory.Limits.Multicoequalizer.multicofork_ΞΉ_app_right, CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_ΞΉ_app, CategoryTheory.Limits.coequalizer.cofork_ΞΉ_app_one, CategoryTheory.Limits.combineCocones_pt_map, CategoryTheory.Limits.Cotrident.ofΟ_ΞΉ_app, CategoryTheory.Functor.LeftExtension.coconeAt_ΞΉ_app, CategoryTheory.Limits.coconeOfIsSplitEpi_ΞΉ_app, PresheafOfModules.colimitCocone_ΞΉ_app_app, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ΞΉ_app_eq_sum, CategoryTheory.SmallObject.coconeOfLE_ΞΉ_app, CategoryTheory.Limits.colimitCoconeOfUnique_cocone_ΞΉ, CategoryTheory.Limits.IsColimit.ΞΉ_app_homEquiv_symm, CategoryTheory.Monad.MonadicityInternal.counitCofork_ΞΉ_app, CategoryTheory.Limits.CokernelCofork.Ο_eq_zero, CategoryTheory.Functor.Final.extendCocone_map_hom, CategoryTheory.Limits.coconeUnopOfCone_ΞΉ, CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ΞΉ_of_isColimit, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_fac, CategoryTheory.Limits.Cofork.ofΟ_ΞΉ_app, ModuleCat.FilteredColimits.ΞΉ_colimitDesc_assoc, eta_hom_hom, CategoryTheory.Limits.coneUnopOfCocone_Ο, CategoryTheory.Limits.Cotrident.app_one_assoc, CategoryTheory.Limits.Multicofork.ofSigmaCofork_ΞΉ_app_left, CategoryTheory.Limits.coconeOfCoconeCurry_ΞΉ_app, CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app, CategoryTheory.FinitaryExtensive.isPullback_initial_to, CategoryTheory.Limits.PreservesColimitβ.ΞΉ_comp_isoObjConePointsOfIsColimit_inv_assoc, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_ΞΉ_app_f, CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc, CategoryTheory.Limits.IsColimit.fac_assoc, AlgebraicGeometry.SheafedSpace.isColimit_exists_rep, CategoryTheory.Limits.pushoutCoconeOfRightIso_ΞΉ_app_right, CategoryTheory.Limits.colimit.isoColimitCocone_ΞΉ_hom, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff', fromStructuredArrow_obj_ΞΉ, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv, TopCat.coconeOfCoconeForget_ΞΉ_app, CategoryTheory.Comma.colimitAuxiliaryCocone_ΞΉ_app, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.wβ, CategoryTheory.Sheaf.sheafifyCocone_ΞΉ_app_val, CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists, CategoryTheory.Limits.Cofork.app_one_eq_Ο, CategoryTheory.Limits.constCocone_ΞΉ, CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ΞΉ_app, underPost_pt, CommRingCat.coproductCocone_ΞΉ, extensions_app, AlgebraicGeometry.PresheafedSpace.colimitCocone_ΞΉ_app_c, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.wβ_assoc, CategoryTheory.Limits.CoconeMorphism.map_w, CategoryTheory.Over.liftCocone_pt, CategoryTheory.Limits.colimit.ΞΉ_desc_app, CategoryTheory.IsPushout.of_isColimit_cocone, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, CategoryTheory.Functor.costructuredArrowMapCocone_ΞΉ_app, SSet.range_eq_iSup_of_isColimit, CategoryTheory.Limits.Cone.op_ΞΉ, CategoryTheory.Monad.ForgetCreatesColimits.newCocone_ΞΉ
|
| Name | Category | Theorems |
category π | CompOp | 281 mathmath: CategoryTheory.Limits.DiagramOfCones.id, CategoryTheory.Functor.Initial.extendCone_obj_pt, CategoryTheory.WithTerminal.coneEquiv_unitIso_hom_app_hom_left, CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc, reflects_cone_isomorphism, CategoryTheory.Limits.ConeMorphism.hom_inv_id, CategoryTheory.Limits.hasLimit_iff_hasTerminal_cone, CategoryTheory.Functor.mapConeMapCone_hom_hom, CategoryTheory.Limits.coneOpEquiv_unitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom, postcomposeComp_hom_app_hom, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_map_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_Ο_app, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_obj, CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_hom, CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from, CategoryTheory.Limits.ConeMorphism.inv_hom_id_assoc, functoriality_full, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_map_hom, CategoryTheory.Limits.coneUnopOfCoconeEquiv_counitIso, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom, CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_hom, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom, postcomposeEquivalence_functor, CategoryTheory.Limits.Multifork.ext_hom_hom, CategoryTheory.Limits.Multifork.isoOfΞΉ_hom_hom, whiskeringEquivalence_functor, functorialityEquivalence_inverse, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_Ο_app_left, postcomposeComp_inv_app_hom, ext_inv_inv_hom, CategoryTheory.Limits.Fork.isoForkOfΞΉ_hom_hom, eta_hom_hom, fromCostructuredArrow_map_hom, toCostructuredArrow_obj, CategoryTheory.Functor.mapConePostcompose_inv_hom, extendIso_hom_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, CategoryTheory.Limits.coconeUnopOfConeEquiv_unitIso, CategoryTheory.Limits.Multifork.isoOfΞΉ_inv_hom, extendId_hom_hom, CategoryTheory.Limits.IsLimit.uniqueUpToIso_inv, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_inv_app_hom_left, CategoryTheory.Over.conePost_obj_Ο_app, cone_iso_of_hom_iso, CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso, forget_obj, CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom, fromCostructuredArrow_obj_Ο, CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom, postcomposeEquivalence_unitIso, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_obj, CategoryTheory.Functor.Initial.conesEquiv_counitIso, postcompose_obj_pt, CategoryTheory.Limits.Fork.ΞΉ_postcompose, CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ΞΉ, CategoryTheory.WithTerminal.coneEquiv_functor_obj_Ο_app_star, CategoryTheory.WithTerminal.coneEquiv_counitIso_inv_app_hom, CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_map_hom, CategoryTheory.Functor.mapCoconeOp_inv_hom, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom, CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor, CategoryTheory.Limits.Wedge.ext_hom_hom, CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ΞΉ, equivCostructuredArrow_inverse, CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, CategoryTheory.Limits.IsLimit.ofIsoLimit_lift, CategoryTheory.Functor.Initial.extendCone_obj_Ο_app', CategoryTheory.Limits.coneOpEquiv_inverse_obj, functorialityEquivalence_counitIso, CategoryTheory.Limits.coconeUnopOfConeEquiv_counitIso, CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_obj, CategoryTheory.WithTerminal.coneEquiv_functor_obj_Ο_app_of, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, CategoryTheory.Over.conePostIso_hom_app_hom, CategoryTheory.Functor.RightExtension.coneAtFunctor_obj, CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_map_hom, category_id_hom, CategoryTheory.Limits.coconeOpEquiv_inverse_map, CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply, CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, CategoryTheory.Limits.coconeOpEquiv_functor_obj, FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone, whiskeringEquivalence_unitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt, postcompose_obj_Ο, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom, CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_map, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_left, whiskering_map_hom, CategoryTheory.Limits.IsLimit.uniqueUpToIso_hom, CategoryTheory.Over.conePost_map_hom, CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_inv_hom, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_obj, postcomposeEquivalence_counitIso, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj, CategoryTheory.Limits.Trident.ext_hom, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, CategoryTheory.Functor.Initial.conesEquiv_unitIso, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_obj, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, CategoryTheory.Limits.Fork.ext_hom, CategoryTheory.Limits.DiagramOfCones.conePoints_map, mapConeToUnder_inv_hom, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom, CategoryTheory.Limits.Cones.functoriality_faithful, CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_obj, extendId_inv_hom, CategoryTheory.Limits.coneOpEquiv_functor_obj, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_hom, CategoryTheory.Limits.Fan.ext_inv_hom, CategoryTheory.Limits.coconeRightOpOfConeEquiv_unitIso, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left, CategoryTheory.Limits.coneOpEquiv_counitIso, CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_map_hom, extendComp_inv_hom, CategoryTheory.Limits.Fan.ext_hom_hom, CategoryTheory.Functor.Initial.extendCone_map_hom, toCostructuredArrow_map, CategoryTheory.Limits.PullbackCone.eta_inv_hom, CategoryTheory.Functor.Initial.conesEquiv_inverse, CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso, CategoryTheory.Limits.Fork.ext_inv, CategoryTheory.Limits.instIsIsoHomInvCone, CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_map, functoriality_obj_Ο_app, CategoryTheory.Limits.PullbackCone.unop_ΞΉ_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, CategoryTheory.Limits.PullbackCone.isoMk_inv_hom, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_map, CategoryTheory.Limits.Cones.functoriality_full, CategoryTheory.Adjunction.functorialityUnit'_app_hom, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_Ο_app, CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_obj, CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso, CategoryTheory.liftedLimitMapsToOriginal_inv_map_Ο, CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_obj, equivalenceOfReindexing_functor, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom, CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj, equivCostructuredArrow_functor, whiskeringEquivalence_counitIso, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_Ο_app, CategoryTheory.Over.conePostIso_inv_app_hom, CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ΞΉ, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, functoriality_obj_pt, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isLimit, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_Ο_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_unitIso, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, CategoryTheory.Limits.PullbackCone.eta_hom_hom, ext_inv_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, CategoryTheory.Over.conePost_obj_pt, CategoryTheory.Limits.coconeOpEquiv_inverse_obj, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, CategoryTheory.Limits.Trident.ext_inv, CategoryTheory.Over.ConstructProducts.conesEquiv_functor, CategoryTheory.Functor.mapConeWhisker_hom_hom, equivCostructuredArrow_counitIso, CategoryTheory.Limits.coneOpEquiv_functor_map_hom, ext_inv_hom_hom, CategoryTheory.Limits.Wedge.ext_inv_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, category_comp_hom, CategoryTheory.Limits.coconeOpEquiv_unitIso, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom, CategoryTheory.Limits.ConeMorphism.hom_inv_id_assoc, ext_hom_hom, functorialityEquivalence_functor, fromCostructuredArrow_obj_pt, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_map_hom, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_obj, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_unitIso, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_map, CategoryTheory.Limits.coconeRightOpOfConeEquiv_counitIso, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, CategoryTheory.Limits.limit.lift_map, CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_obj, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, CategoryTheory.Functor.RightExtension.coneAtFunctor_map_hom, whiskering_obj, CategoryTheory.Functor.mapConePostcompose_hom_hom, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_inv, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt, CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_hom_hom, CategoryTheory.Limits.coneOpEquiv_inverse_map, CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj, CategoryTheory.WithTerminal.coneEquiv_unitIso_inv_app_hom_left, CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_obj, CategoryTheory.Limits.DiagramOfCones.comp, CategoryTheory.Functor.mapCoconeOp_hom_hom, equivalenceOfReindexing_counitIso, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_hom_app_hom, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_counitIso, equivalenceOfReindexing_unitIso, mapConeToUnder_hom_hom, functoriality_map_hom, CategoryTheory.Over.ConstructProducts.conesEquivInverse_obj, postcomposeId_inv_app_hom, CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_map, CategoryTheory.Functor.Initial.limitConeOfComp_cone, equivCostructuredArrow_unitIso, instIsIsoExtendHom, equivalenceOfReindexing_inverse, CategoryTheory.Limits.coconeOpEquiv_counitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom, extendComp_hom_hom, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_counitIso, CategoryTheory.Limits.Multifork.ext_inv_hom, CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left, CategoryTheory.Functor.mapConeMapCone_inv_hom, CategoryTheory.Limits.BinaryFan.ext_hom_hom, CategoryTheory.Limits.PullbackCone.isoMk_hom_hom, CategoryTheory.Functor.Initial.extendCone_obj_Ο_app, extendIso_inv_hom, CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom, CategoryTheory.Limits.Fork.isoForkOfΞΉ_inv_hom, postcomposeId_hom_app_hom, CategoryTheory.Functor.mapConeWhisker_inv_hom, forget_map, CategoryTheory.WithTerminal.coneEquiv_functor_obj_pt, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_unitIso, CategoryTheory.Over.ConstructProducts.conesEquiv_inverse, CategoryTheory.liftedLimitMapsToOriginal_hom_Ο, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso, whiskeringEquivalence_inverse, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv, CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ΞΉ, CategoryTheory.Limits.limit.lift_map_assoc, CategoryTheory.Limits.Cones.reflects_cone_isomorphism, CategoryTheory.Functor.Initial.conesEquiv_functor, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, postcomposeEquivalence_inverse, CategoryTheory.Limits.Cones.cone_iso_of_hom_iso, postcompose_map_hom, eta_inv_hom, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom_assoc, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_map, functoriality_faithful, CategoryTheory.Limits.coconeOpEquiv_functor_map_hom, CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism, FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone, CategoryTheory.Limits.coneUnopOfCoconeEquiv_unitIso, CategoryTheory.WithTerminal.coneEquiv_counitIso_hom_app_hom, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_obj, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_Ο_app, CategoryTheory.Limits.IsLimit.hom_isIso, CategoryTheory.Functor.Initial.limitConeOfComp_isLimit, CategoryTheory.Limits.instIsIsoHomHomCone, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom, CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom, CategoryTheory.Adjunction.functorialityCounit'_app_hom, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_right_as, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_counitIso, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv_assoc, CategoryTheory.Limits.ConeMorphism.inv_hom_id, CategoryTheory.WithTerminal.coneEquiv_functor_map_hom, functorialityEquivalence_unitIso
|
equiv π | CompOp | 4 mathmath: equiv_inv_pt, equiv_hom_fst, equiv_inv_Ο, equiv_hom_snd
|
equivalenceOfReindexing π | CompOp | 6 mathmath: equivalenceOfReindexing_functor, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_inv, equivalenceOfReindexing_counitIso, equivalenceOfReindexing_unitIso, equivalenceOfReindexing_inverse
|
eta π | CompOp | 3 mathmath: eta_hom_hom, equivCostructuredArrow_unitIso, eta_inv_hom
|
ext π | CompOp | 14 mathmath: postcomposeEquivalence_unitIso, CategoryTheory.Functor.Initial.conesEquiv_counitIso, functorialityEquivalence_counitIso, whiskeringEquivalence_unitIso, postcomposeEquivalence_counitIso, CategoryTheory.Functor.Initial.conesEquiv_unitIso, whiskeringEquivalence_counitIso, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isLimit, ext_inv_hom, ext_hom_hom, equivalenceOfReindexing_counitIso, equivalenceOfReindexing_unitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, functorialityEquivalence_unitIso
|
ext_inv π | CompOp | 2 mathmath: ext_inv_inv_hom, ext_inv_hom_hom
|
extend π | CompOp | 15 mathmath: extendIso_hom_hom, extendId_hom_hom, extend_Ο, extend_pt, CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac, extendHom_hom, extendId_inv_hom, extendComp_inv_hom, CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac, instIsIsoExtendHom, extendComp_hom_hom, extendIso_inv_hom, CategoryTheory.Limits.IsLimit.homIso_hom, CategoryTheory.Limits.limit.lift_extend, CategoryTheory.Limits.IsLimit.homEquiv_apply
|
extendComp π | CompOp | 2 mathmath: extendComp_inv_hom, extendComp_hom_hom
|
extendHom π | CompOp | 2 mathmath: extendHom_hom, instIsIsoExtendHom
|
extendId π | CompOp | 2 mathmath: extendId_hom_hom, extendId_inv_hom
|
extendIso π | CompOp | 2 mathmath: extendIso_hom_hom, extendIso_inv_hom
|
extensions π | CompOp | 1 mathmath: extensions_app
|
forget π | CompOp | 2 mathmath: forget_obj, forget_map
|
functoriality π | CompOp | 21 mathmath: reflects_cone_isomorphism, functoriality_full, functorialityEquivalence_inverse, CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom, functorialityEquivalence_counitIso, CategoryTheory.Over.conePostIso_hom_app_hom, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom, CategoryTheory.Limits.Cones.functoriality_faithful, functoriality_obj_Ο_app, CategoryTheory.Limits.Cones.functoriality_full, CategoryTheory.Adjunction.functorialityUnit'_app_hom, CategoryTheory.Over.conePostIso_inv_app_hom, functoriality_obj_pt, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom, functorialityEquivalence_functor, functoriality_map_hom, CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom, CategoryTheory.Limits.Cones.reflects_cone_isomorphism, functoriality_faithful, CategoryTheory.Adjunction.functorialityCounit'_app_hom, functorialityEquivalence_unitIso
|
functorialityCompFunctoriality π | CompOp | β |
functorialityEquivalence π | CompOp | 4 mathmath: functorialityEquivalence_inverse, functorialityEquivalence_counitIso, functorialityEquivalence_functor, functorialityEquivalence_unitIso
|
op π | CompOp | 13 mathmath: CategoryTheory.Limits.PullbackCone.op_ΞΉ_app, Condensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.coneOpEquiv_functor_obj, CategoryTheory.Limits.coneOpEquiv_counitIso, CategoryTheory.Limits.Fork.op_ΞΉ_app, CategoryTheory.Limits.coneOpEquiv_functor_map_hom, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Functor.mapConeOp_inv_hom, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Functor.mapConeOp_hom_hom, op_pt, AlgebraicGeometry.nonempty_isColimit_Ξ_mapCocone, op_ΞΉ
|
postcompose π | CompOp | 39 mathmath: CategoryTheory.Limits.DiagramOfCones.id, postcomposeComp_hom_app_hom, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom, postcomposeEquivalence_functor, postcomposeComp_inv_app_hom, CategoryTheory.Functor.mapConePostcompose_inv_hom, CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom, postcomposeEquivalence_unitIso, postcompose_obj_pt, CategoryTheory.Limits.Fork.ΞΉ_postcompose, CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom, whiskeringEquivalence_unitIso, postcompose_obj_Ο, postcomposeEquivalence_counitIso, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom, CategoryTheory.Limits.DiagramOfCones.conePoints_map, CategoryTheory.Limits.PullbackCone.unop_ΞΉ_app, CategoryTheory.Limits.PullbackCone.isoMk_inv_hom, equivalenceOfReindexing_functor, whiskeringEquivalence_counitIso, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isLimit, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom, CategoryTheory.Limits.limit.lift_map, CategoryTheory.Functor.mapConePostcompose_hom_hom, CategoryTheory.Limits.DiagramOfCones.comp, equivalenceOfReindexing_counitIso, equivalenceOfReindexing_unitIso, postcomposeId_inv_app_hom, equivalenceOfReindexing_inverse, CategoryTheory.Limits.PullbackCone.isoMk_hom_hom, CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom, postcomposeId_hom_app_hom, whiskeringEquivalence_inverse, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv, CategoryTheory.Limits.limit.lift_map_assoc, postcomposeEquivalence_inverse, postcompose_map_hom, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom_assoc, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv_assoc
|
postcomposeComp π | CompOp | 2 mathmath: postcomposeComp_hom_app_hom, postcomposeComp_inv_app_hom
|
postcomposeEquivalence π | CompOp | 9 mathmath: postcomposeEquivalence_functor, functorialityEquivalence_inverse, postcomposeEquivalence_unitIso, functorialityEquivalence_counitIso, postcomposeEquivalence_counitIso, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom, postcomposeEquivalence_inverse, functorialityEquivalence_unitIso
|
postcomposeId π | CompOp | 2 mathmath: postcomposeId_inv_app_hom, postcomposeId_hom_app_hom
|
pt π | CompOp | 904 mathmath: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, CategoryTheory.Limits.Trident.condition_assoc, CategoryTheory.Limits.Fork.IsLimit.homIso_natural, CategoryTheory.Limits.DiagramOfCones.id, CategoryTheory.PreOneHypercover.forkOfIsColimit_ΞΉ_map_inj_assoc, CategoryTheory.Functor.Initial.extendCone_obj_pt, toUnder_pt, CategoryTheory.WithTerminal.coneEquiv_unitIso_hom_app_hom_left, CategoryTheory.Functor.coneOfIsRightKanExtension_pt, CategoryTheory.Limits.BinaryFan.rightUnitor_hom, CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc, AddCommGrpCat.binaryProductLimitCone_cone_pt, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac, LightProfinite.Extend.functorOp_obj, CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback', CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc, CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_pt, CategoryTheory.Limits.ConeMorphism.hom_inv_id, CategoryTheory.extendFan_pt, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, CategoryTheory.Functor.mapConeMapCone_hom_hom, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp_assoc, CategoryTheory.Limits.Wedge.mk_pt, CategoryTheory.Limits.Trident.app_zero, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom, AlgebraicGeometry.opensCone_pt, postcomposeComp_hom_app_hom, unop_ΞΉ, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, ofTrident_Ο, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_map_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_Ο_app, CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_hom, CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val, CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, CategoryTheory.Limits.Fork.IsLimit.lift_ΞΉ'_assoc, CategoryTheory.Limits.ConeMorphism.inv_hom_id_assoc, CategoryTheory.Limits.pullbackConeOfLeftIso_Ο_app_left, CategoryTheory.PreOneHypercover.forkOfIsColimit_pt, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc, CategoryTheory.Functor.isLimitConeOfIsRightKanExtension_lift, Profinite.Extend.functorOp_map, CategoryTheory.Functor.isCardinalAccessible_of_isLimit, CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, CategoryTheory.biconeMk_obj, CategoryTheory.Limits.coneUnopOfCoconeEquiv_counitIso, HomologicalComplex.coneOfHasLimitEval_pt_d, CategoryTheory.ObjectProperty.prop_of_isLimit_kernelFork, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_Ο, CategoryTheory.Limits.BinaryBicone.toCone_Ο_app_right, CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map', CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom, CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj, equiv_inv_pt, CategoryTheory.Limits.Types.limitCone_pt, CategoryTheory.Limits.BinaryFan.braiding_hom_snd_assoc, CategoryTheory.Comonad.beckCoalgebraFork_pt, CategoryTheory.Limits.IsLimit.map_Ο, CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_hom, CategoryTheory.Comonad.ComonadicityInternal.unitFork_pt, CategoryTheory.Limits.mono_of_isLimit_parallelFamily, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc, CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_Ο_app_f, CategoryTheory.Limits.PullbackCone.Ο_app_right, Preorder.conePt_mem_lowerBounds, CategoryTheory.Limits.Multifork.ext_hom_hom, CategoryTheory.Limits.Multifork.isoOfΞΉ_hom_hom, CategoryTheory.Limits.Fork.unop_ΞΉ_app_zero, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_pos_assoc, CategoryTheory.isCoseparator_of_isLimit_fan, CategoryTheory.Limits.KernelFork.condition_assoc, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_Ο_app_left, postcomposeComp_inv_app_hom, CategoryTheory.Limits.KernelFork.mapOfIsLimit_ΞΉ_assoc, CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_Ο, ext_inv_inv_hom, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom, CategoryTheory.Limits.Fork.isoForkOfΞΉ_hom_hom, CategoryTheory.Functor.RightExtension.coneAt_pt, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.BinaryFan.braiding_hom_fst_assoc, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc, CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.fac, CategoryTheory.Limits.Fork.IsLimit.mono, eta_hom_hom, toCostructuredArrow_obj, CategoryTheory.Limits.kernel.zeroKernelFork_ΞΉ, CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono, CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom, CategoryTheory.Limits.WidePullbackCone.reindex_pt, CategoryTheory.Functor.mapConePostcompose_inv_hom, CategoryTheory.Comma.coneOfPreserves_Ο_app_right, CategoryTheory.Comma.limitAuxiliaryCone_pt, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_Ο_app_walkingParallelPair_one, CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc, extendIso_hom_hom, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_K, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, CategoryTheory.FunctorToTypes.binaryProductCone_pt_obj, CategoryTheory.Limits.coconeOfConeLeftOp_pt, CategoryTheory.Limits.constCone_pt, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, whisker_Ο, CategoryTheory.Limits.Multifork.isoOfΞΉ_inv_hom, extendId_hom_hom, CompHausLike.pullback.isLimit_lift, CategoryTheory.Under.liftCone_pt, CategoryTheory.Limits.PullbackCone.unop_inl, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsColimit_inv_comp_map_Ο, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom, CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift, CategoryTheory.ObjectProperty.prop_of_isLimit, toStructuredArrowCompProj_inv_app, AlgebraicGeometry.Scheme.Pullback.gluedLift_p1, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp, CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_inv_app_hom_left, CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst, CategoryTheory.Limits.Trident.ofΞΉ_pt, CategoryTheory.Limits.Fork.ofΞΉ_pt, CategoryTheory.Over.conePost_obj_Ο_app, CategoryTheory.Limits.PullbackCone.op_pt, CategoryTheory.Limits.Types.binaryProductCone_pt, CategoryTheory.Limits.coneUnopOfCocone_pt, CategoryTheory.Limits.Cofork.unop_Ο_app_one, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl, CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift, CategoryTheory.Limits.pullbackConeOfLeftIso_Ο_app_right, forget_obj, CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom_assoc, CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom, Profinite.exists_locallyConstant_finite_aux, CategoryTheory.Mon.limitConeIsLimit_lift_hom, CategoryTheory.Limits.IsLimit.nonempty_isLimit_iff_isIso_lift, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_pt, GrpCat.binaryProductLimitCone_cone_pt, CategoryTheory.Limits.opCoproductIsoProduct'_comp_self, CategoryTheory.Limits.pullbackConeOfLeftIso_snd, CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom, CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj, CategoryTheory.ProdPreservesConnectedLimits.forgetCone_Ο, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_Ο_app, CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Limits.limit.lift_post, postcomposeEquivalence_unitIso, lightDiagramToLightProfinite_obj, CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv, extend_Ο, CategoryTheory.Functor.Initial.conesEquiv_counitIso, Profinite.isIso_indexCone_lift, CategoryTheory.Limits.Bicone.toCone_Ο_app_mk, CategoryTheory.Limits.Multifork.ofΞΉ_pt, CategoryTheory.Limits.PullbackCone.condition_assoc, CategoryTheory.Limits.Trident.condition, CategoryTheory.Limits.PullbackCone.unop_inr, CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom, postcompose_obj_pt, CategoryTheory.Limits.Fork.ΞΉ_postcompose, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyΟ_isoHomology_inv_assoc, CategoryTheory.Limits.BinaryBicone.toCone_Ο_app_left, CategoryTheory.Limits.coconeOfConeUnop_pt, CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ΞΉ, CategoryTheory.WithTerminal.coneEquiv_functor_obj_Ο_app_star, Profinite.Extend.functorOp_obj, CategoryTheory.WithTerminal.coneEquiv_counitIso_inv_app_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_H, CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_map_hom, CategoryTheory.Monad.ForgetCreatesLimits.newCone_Ο_app, ModuleCat.binaryProductLimitCone_cone_Ο_app_right, CategoryTheory.Limits.Fork.IsLimit.existsUnique, toStructuredArrowCompToUnderCompForget_hom_app, CategoryTheory.Limits.PullbackCone.combine_Ο_app, CategoryTheory.Limits.Cocone.op_pt, LightProfinite.lightToProfinite_map_proj_eq, CompHausLike.sigmaComparison_eq_comp_isos, CategoryTheory.Limits.Fork.hom_comp_ΞΉ, CategoryTheory.Limits.asEmptyCone_pt, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.associator_naturality, CategoryTheory.Limits.Multiequalizer.multifork_Ο_app_left, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom, CategoryTheory.Limits.ConeMorphism.map_w_assoc, CategoryTheory.Limits.coneOfDiagramTerminal_pt, CategoryTheory.Cat.HasLimits.limitCone_pt, CategoryTheory.Limits.BinaryFan.braiding_hom_snd, CategoryTheory.Limits.limit.isoLimitCone_hom_Ο_assoc, CategoryTheory.Limits.Multifork.toPiFork_pt, CategoryTheory.Limits.PullbackCone.op_inr, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_Ο_app, AlgebraicGeometry.isBasis_preimage_isAffineOpen, CategoryTheory.Limits.coneOfDiagramInitial_pt, CategoryTheory.Limits.PullbackCone.op_ΞΉ_app, CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor, CategoryTheory.Limits.coneOfConeCurry_pt, CategoryTheory.Limits.Wedge.IsLimit.lift_ΞΉ, CategoryTheory.Limits.Fork.unop_ΞΉ_app_one, CategoryTheory.Limits.Wedge.ext_hom_hom, CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, AlgebraicGeometry.Scheme.Pullback.gluedLift_p2, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi, CategoryTheory.Limits.IsLimit.ofIsoLimit_lift, CategoryTheory.Limits.IsLimit.pushout_zero_ext, CategoryTheory.Functor.Initial.extendCone_obj_Ο_app', CategoryTheory.Limits.Fork.IsLimit.homIso_symm_apply, functorialityEquivalence_counitIso, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base, AddCommGrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Limits.Types.Small.limitCone_pt, fromStructuredArrow_pt, toStructuredArrow_comp_toUnder_comp_forget, CategoryTheory.Mon.limit_mon_mul, CategoryTheory.Limits.BinaryFan.braiding_inv_snd, CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono, CategoryTheory.Limits.coconeUnopOfConeEquiv_counitIso, AddCommGrpCat.binaryProductLimitCone_cone_Ο_app_left, CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer', CategoryTheory.Limits.Types.isLimitEquivSections_apply, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_neg_assoc, extend_pt, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_Ο_app_eq_sum, CategoryTheory.WithTerminal.coneEquiv_functor_obj_Ο_app_of, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, CategoryTheory.Comma.coneOfPreserves_pt_right, CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj, ofPullbackCone_pt, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForgetβContinuousAddMonoidHomToProfiniteContinuousMap, CategoryTheory.Limits.IsLimit.homEquiv_symm_Ο_app, CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj, GrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac, CategoryTheory.Preadditive.forkOfKernelFork_pt, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac, CategoryTheory.Over.conePostIso_hom_app_hom, CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc, TopCat.nonempty_isLimit_iff_eq_induced, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, AddCommGrpCat.HasLimit.productLimitCone_cone_pt_coe, CategoryTheory.Limits.Fork.op_pt, CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit, ofPullbackCone_Ο, AlgebraicGeometry.exists_appTop_Ο_eq_of_isAffine_of_isLimit, CategoryTheory.Limits.ConeMorphism.map_w, ProfiniteGrp.cone_pt, TopCat.piFan_pt, CategoryTheory.Limits.limit.isoLimitCone_hom_Ο, CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_map_hom, CategoryTheory.Limits.pullbackConeOfRightIso_Ο_app_right, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K, category_id_hom, CategoryTheory.Functor.rightAdjointObjIsDefined_of_isLimit, CategoryTheory.Limits.IsLimit.hom_lift, CategoryTheory.Limits.coconeOpEquiv_inverse_map, CategoryTheory.Limits.PullbackCone.mk_Ο_app_right, CategoryTheory.Limits.Cofork.op_Ο_app_zero, CategoryTheory.Limits.coneOfConeCurry_Ο_app, CategoryTheory.Sheaf.isSheaf_of_isLimit, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc, CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_pt, AddGrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Limits.pullbackConeOfRightIso_fst, CategoryTheory.lift_comp_preservesLimitIso_hom_assoc, whiskeringEquivalence_unitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt, postcompose_obj_Ο, equiv_hom_fst, CategoryTheory.ObjectProperty.prop_of_isLimit_fan, toStructuredArrowCone_Ο_app, Condensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.Fork.hom_comp_ΞΉ_assoc, Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceΟAsLimitCone, Preorder.coneOfLowerBound_pt, CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsLimit_hom_comp_Ο, CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit_inv, CategoryTheory.Under.forgetCone_pt, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp_assoc, CategoryTheory.Limits.BinaryFan.rightUnitor_inv, CategoryTheory.Limits.pullbackConeOfRightIso_x, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id, CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj_assoc, CategoryTheory.Limits.PullbackCone.mk_Ο_app_one, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_left, TopCat.Sheaf.interUnionPullbackConeLift_right, LightProfinite.Extend.functor_map, CategoryTheory.Limits.CompleteLattice.limitCone_isLimit_lift, CategoryTheory.Over.conePost_map_hom, CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt, CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Limits.Fork.ofCone_Ο, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift, CategoryTheory.Limits.opProductIsoCoproduct'_comp_self, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_obj, postcomposeEquivalence_counitIso, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj, AlgebraicGeometry.exists_preimage_eq, CategoryTheory.Limits.KernelFork.IsLimit.isIso_ΞΉ, CategoryTheory.Limits.Trident.ext_hom, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom, CategoryTheory.Abelian.epi_snd_of_isLimit, CategoryTheory.Limits.coneOfSectionCompYoneda_pt, CategoryTheory.Limits.Types.limitConeIsLimit_lift_coe, CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom, CategoryTheory.Limits.coneOfAdj_pt, CategoryTheory.Functor.Initial.conesEquiv_unitIso, CategoryTheory.Limits.WidePullbackShape.mkCone_pt, CategoryTheory.lift_comp_preservesLimitIso_hom, CategoryTheory.RanIsSheafOfIsCocontinuous.fac', CategoryTheory.Limits.KernelFork.condition, Profinite.exists_isClopen_of_cofiltered, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc, CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_map, CategoryTheory.Limits.Fork.IsLimit.homIso_apply_coe, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd, CategoryTheory.Limits.coneOfCoconeLeftOp_pt, CategoryTheory.Limits.limit.cone_x, CategoryTheory.Limits.Fork.IsLimit.lift_ΞΉ, CategoryTheory.Limits.Fork.ext_hom, CategoryTheory.ShortComplex.LeftHomologyData.wΟ_assoc, CategoryTheory.Limits.Multifork.app_right_eq_ΞΉ_comp_snd, mapConeToUnder_inv_hom, CategoryTheory.Limits.PullbackCone.Ο_app_left, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_pt, CategoryTheory.Limits.Wedge.condition, CategoryTheory.FunctorToTypes.binaryProductLimit_lift, CategoryTheory.Limits.limit.existsUnique, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv, CategoryTheory.Limits.Multifork.app_left_eq_ΞΉ, CategoryTheory.Limits.Multifork.condition, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.leftUnitor_naturality, CategoryTheory.Limits.coconeOfConeRightOp_ΞΉ, CategoryTheory.Limits.limitConeOfUnique_cone_pt, CategoryTheory.Limits.Fork.op_Ο, CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp_assoc, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom, CategoryTheory.Under.liftCone_Ο_app, CategoryTheory.Limits.Wedge.IsLimit.lift_ΞΉ_assoc, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id, CategoryTheory.Limits.Fork.app_one_eq_ΞΉ_comp_left, CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_pt, CategoryTheory.Mon.limitCone_Ο_app_hom, CategoryTheory.Comma.limitAuxiliaryCone_Ο_app, extendId_inv_hom, CategoryTheory.Limits.Trident.IsLimit.homIso_apply_coe, CategoryTheory.Limits.WidePullbackCone.mk_pt, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_hom, CategoryTheory.Limits.Fan.ext_inv_hom, CategoryTheory.Limits.Bicone.toCone_pt, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left, CategoryTheory.Limits.coneOpEquiv_counitIso, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsColimit_inv_comp_map_Ο_assoc, extendComp_inv_hom, CategoryTheory.Limits.Multifork.IsLimit.fac_assoc, Profinite.Extend.functor_obj, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_f_coe, CategoryTheory.Limits.Fan.ext_hom_hom, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_Ο_assoc, CategoryTheory.Functor.Initial.extendCone_map_hom, toCostructuredArrow_map, CategoryTheory.Limits.BinaryFan.Ο_app_right, AlgebraicGeometry.opensCone_Ο_app, CategoryTheory.Limits.PullbackCone.eta_inv_hom, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_auxβ, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst, CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective, CategoryTheory.Limits.Fan.IsLimit.fac_assoc, CategoryTheory.Limits.PushoutCocone.op_Ο_app, CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_Ο, CategoryTheory.Limits.limit.lift_Ο_app, CategoryTheory.biconeMk_map, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt, CategoryTheory.Limits.WidePullbackCone.condition_assoc, PresheafOfModules.isSheaf_of_isLimit, CategoryTheory.Limits.Fork.ext_inv, CategoryTheory.Limits.Fork.app_one_eq_ΞΉ_comp_right_assoc, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base_assoc, CategoryTheory.Limits.instIsIsoHomInvCone, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv, overPost_pt, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, CategoryTheory.Functor.Initial.limit_cone_comp_aux, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.triangle, CategoryTheory.Sheaf.coneΞ_pt, CategoryTheory.Preadditive.mono_iff_isZero_kernel', CategoryTheory.Limits.coneOfSectionCompCoyoneda_pt, CategoryTheory.Over.liftCone_Ο_app, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_Ο, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, CategoryTheory.Limits.isLimitConeOfAdj_lift, CategoryTheory.Limits.Types.Limit.lift_Ο_apply, CategoryTheory.Limits.BinaryFan.braiding_inv_fst_assoc, functoriality_obj_Ο_app, CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift, CategoryTheory.Limits.ConeMorphism.w_assoc, CategoryTheory.Limits.PullbackCone.unop_ΞΉ_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, CategoryTheory.Limits.BinaryBicone.toCone_pt, CategoryTheory.Limits.Multifork.toPiFork_Ο_app_one, CategoryTheory.Limits.Multifork.ofPiFork_pt, CategoryTheory.Limits.pullbackConeOfLeftIso_Ο_app_none, CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom, CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit, CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq, CategoryTheory.Limits.Fan.IsLimit.fac, CategoryTheory.Functor.mapCone_pt, CategoryTheory.Limits.PullbackCone.isoMk_inv_hom, CategoryTheory.Limits.coconeOfConeRightOp_pt, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_map, CategoryTheory.Functor.mapConeβ_pt, CategoryTheory.ProdPreservesConnectedLimits.forgetCone_pt, CategoryTheory.Limits.kernel.zeroKernelFork_pt, CategoryTheory.Limits.limit.isoLimitCone_inv_Ο_assoc, CategoryTheory.Limits.BinaryFan.braiding_hom_fst, Algebra.codRestrictEqLocusPushoutCocone.surjective_of_isEffective, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_auxβ, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Adjunction.functorialityUnit'_app_hom, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_Ο, CategoryTheory.Functor.mapConeβ_Ο_app, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_pos, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsLimit_hom_comp_Ο_assoc, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_Ο_app, CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv_assoc, LightProfinite.Extend.functorOp_map, TopCat.Sheaf.interUnionPullbackConeLift_left, CategoryTheory.Limits.coneOfCoconeRightOp_pt, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst, Alexandrov.lowerCone_Ο_app, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', CategoryTheory.Limits.Fork.condition, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc, CategoryTheory.ShortComplex.LeftHomologyData.wΟ, ModuleCat.binaryProductLimitCone_cone_Ο_app_left, CategoryTheory.liftedLimitMapsToOriginal_inv_map_Ο, CategoryTheory.Limits.KernelFork.app_one, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, CategoryTheory.Functor.coneOfIsRightKanExtension_Ο, CategoryTheory.Limits.Fork.app_zero_eq_ΞΉ, CategoryTheory.Limits.limit.cone_Ο, CategoryTheory.Limits.IsLimit.isIso_limMap_Ο, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom, CategoryTheory.Limits.limit.lift_Ο_apply, CategoryTheory.Limits.DiagramOfCones.conePoints_obj, CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift, CategoryTheory.Limits.isKernelCompMono_lift, CategoryTheory.Limits.pullbackConeOfRightIso_Ο_app_left, CategoryTheory.Limits.pullbackConeOfLeftIso_x, toStructuredArrowCompProj_hom_app, CategoryTheory.Limits.Trident.ofCone_Ο, CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom, CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp, CategoryTheory.IsSplitEqualizer.asFork_pt, CategoryTheory.Functor.mapCone_Ο_app, CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj, whiskeringEquivalence_counitIso, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_Ο_app, CategoryTheory.Over.conePostIso_inv_app_hom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion, CategoryTheory.Sheaf.coneΞ_Ο_app, CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ΞΉ, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, CategoryTheory.Limits.coneOfConeUncurry_Ο_app, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt, CategoryTheory.Abelian.AbelianStruct.ΞΉ_imageΟ_assoc, functoriality_obj_pt, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt, CategoryTheory.Limits.Fork.op_ΞΉ_app, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse, CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isLimit, CategoryTheory.Functor.IsEventuallyConstantTo.isIso_Ο_of_isLimit, CategoryTheory.Functor.IsEventuallyConstantTo.cone_pt, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_Ο_app, CategoryTheory.Limits.Pi.map_eq_prod_map, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac_assoc, CategoryTheory.Limits.coconeUnopOfCone_pt, CategoryTheory.Limits.Concrete.surjective_Ο_app_zero_of_surjective_map, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, Profinite.exists_locallyConstant, CategoryTheory.Limits.Trident.equalizer_ext, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_Ο_app, CategoryTheory.Limits.Multifork.IsLimit.fac, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.extendFan_Ο_app, CategoryTheory.Limits.coneRightOpOfCocone_pt, CommGrpCat.binaryProductLimitCone_cone_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, CategoryTheory.Limits.PullbackCone.eta_hom_hom, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_snd, CategoryTheory.Limits.BinaryBicone.ofLimitCone_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, ext_inv_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Over.conePost_obj_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, CategoryTheory.Limits.limitConeOfUnique_isLimit_lift, CategoryTheory.coherentTopology.epi_Ο_app_zero_of_epi, CategoryTheory.Limits.coneLeftOpOfCocone_pt, CategoryTheory.Limits.Trident.ΞΉ_eq_app_zero, CategoryTheory.Limits.limit.lift_pre, CategoryTheory.Limits.Fork.op_ΞΉ_app_one, w, CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.Limits.PullbackCone.ofCone_Ο, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, CategoryTheory.Limits.Trident.ext_inv, CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst, CategoryTheory.Limits.PullbackCone.op_inl, CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd, CategoryTheory.Functor.mapConeWhisker_hom_hom, AlgebraicGeometry.ExistsHomHomCompEqCompAux.hab, ModuleCat.HasLimit.productLimitCone_cone_pt_isModule, CategoryTheory.Limits.Cofork.unop_Ο_app_zero, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ΞΉ_assoc, CategoryTheory.Limits.coneOpEquiv_functor_map_hom, toStructuredArrow_obj, Algebra.codRestrictEqLocusPushoutCocone.injective_of_faithfulSMul, ext_inv_hom_hom, CategoryTheory.Over.isPullback_of_binaryFan_isLimit, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv, CategoryTheory.Limits.IsLimit.fac_assoc, CategoryTheory.Limits.PullbackCone.flip_pt, CategoryTheory.Limits.BinaryFan.braiding_inv_fst, CategoryTheory.Limits.Wedge.ext_inv_hom, CategoryTheory.Limits.BinaryFan.assoc_snd, CategoryTheory.Limits.Pi.cone_pt, CategoryTheory.Limits.IsLimit.homEquiv_symm_Ο_app_assoc, Profinite.Extend.functorOp_final, category_comp_hom, CategoryTheory.Limits.CoproductDisjoint.nonempty_isInitial_of_ne, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.pentagon, CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_f, CategoryTheory.Monad.ForgetCreatesLimits.conePoint_A, CategoryTheory.Comma.coneOfPreserves_pt_hom, ModuleCat.HasLimit.productLimitCone_cone_pt_carrier, CategoryTheory.Limits.Trident.IsLimit.homIso_symm_apply, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom, CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom_pt, CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj_assoc, CategoryTheory.Limits.ConeMorphism.hom_inv_id_assoc, TopCat.coneOfConeForget_Ο_app, CategoryTheory.Limits.BinaryFan.braiding_inv_snd_assoc, CategoryTheory.Limits.Bicone.ofLimitCone_Ο, ext_hom_hom, CategoryTheory.Limits.Fan.IsLimit.lift_proj, ofFork_Ο, CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc, CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_K, TopCat.induced_of_isLimit, CategoryTheory.Limits.Types.surjective_Ο_app_zero_of_surjective_map, CategoryTheory.Limits.coconeLeftOpOfCone_ΞΉ_app, AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty', fromCostructuredArrow_obj_pt, isLimit_iff_isIso_limMap_Ο, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, CategoryTheory.MorphismProperty.limitsOfShape.mk', CategoryTheory.Limits.coconeRightOpOfCone_ΞΉ, CategoryTheory.Limits.PullbackCone.combine_pt_map, CategoryTheory.Limits.Fork.IsLimit.lift_ΞΉ_assoc, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_map, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.PullbackCone.equalizer_ext, CategoryTheory.Limits.Multifork.app_right_eq_ΞΉ_comp_snd_assoc, CategoryTheory.Limits.PullbackCone.unop_pt, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_id, CategoryTheory.Limits.coconeRightOpOfConeEquiv_counitIso, CategoryTheory.Limits.limit.lift_Ο_assoc, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, CategoryTheory.Limits.Fork.IsLimit.lift_ΞΉ', CategoryTheory.Mon.limit_X, CategoryTheory.Limits.limit.pre_eq, CategoryTheory.Limits.limit.lift_map, AddCommGrpCat.HasLimit.lift_hom_apply, CategoryTheory.Limits.PullbackCone.combine_pt_obj, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom, CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, CategoryTheory.Limits.PushoutCocone.op_pt, CategoryTheory.Limits.Multifork.ofPiFork_Ο_app_right, LightCondensed.epi_Ο_app_zero_of_epi, CategoryTheory.Functor.mapConeOp_inv_hom, CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition, CategoryTheory.Limits.Multifork.ofPiFork_Ο_app_left, CategoryTheory.regularTopology.equalizerCondition_w, CategoryTheory.Functor.mapConePostcompose_hom_hom, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles, CategoryTheory.Subfunctor.equalizer.fork_pt, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_inv, AlgebraicGeometry.exists_appTop_Ο_eq_of_isLimit, TopCat.Presheaf.isGluing_iff_pairwise, Alexandrov.lowerCone_pt, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt, CategoryTheory.Limits.pullbackConeOfRightIso_Ο_app_none, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fst, HomologicalComplex.quasiIsoAt_Ο_of_isLimit_of_isEventuallyConstantTo, CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv_assoc, HomologicalComplex.coneOfHasLimitEval_pt_X, whisker_pt, CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer', ModuleCat.HasLimit.lift_hom_apply, ModuleCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Comonad.beckEqualizer_lift, CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_A, CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj, Profinite.Extend.cone_pt, CategoryTheory.isCoseparator_iff_of_isLimit_fan, CategoryTheory.WithTerminal.coneEquiv_unitIso_inv_app_hom_left, lightDiagramToLightProfinite_map, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right, CategoryTheory.RanIsSheafOfIsCocontinuous.fac, CategoryTheory.Limits.limit.isoLimitCone_inv_Ο, CategoryTheory.Limits.Bicone.toCone_Ο_app, CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_Ο, CategoryTheory.Limits.BinaryFan.leftUnitor_hom, CategoryTheory.Subobject.leInfCone_Ο_app_none, CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift, unop_pt, CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom_assoc, CategoryTheory.Limits.DiagramOfCones.comp, CategoryTheory.Limits.PullbackCone.condition_one, CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_Ο_app, equivalenceOfReindexing_counitIso, CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.condition, CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer', CategoryTheory.Presieve.piComparison_fac, CategoryTheory.Limits.BinaryBicone.ofLimitCone_fst, toUnder_Ο_app, CategoryTheory.Limits.IsLimit.assoc_lift, CategoryTheory.Comonad.beckFork_pt, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp_assoc, CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_obj, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_hom_app_hom, AlgebraicGeometry.Scheme.nonempty_of_isLimit, CategoryTheory.Limits.coconeOfConeLeftOp_ΞΉ_app, CategoryTheory.Limits.limit.coneMorphism_Ο, CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_counitIso, CategoryTheory.Limits.KernelFork.map_condition, AlgebraicGeometry.Scheme.compactSpace_of_isLimit, CategoryTheory.Limits.coconeOfConeUnop_ΞΉ, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyΟ_isoHomology_inv, CategoryTheory.Limits.IsLimit.lift_self, CategoryTheory.Mon.limitCone_pt, equivalenceOfReindexing_unitIso, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty, CommRingCat.piFan_pt, CategoryTheory.Limits.Fork.op_ΞΉ_app_zero, AlgebraicGeometry.Scheme.exists_Ο_app_comp_eq_of_locallyOfFinitePresentation, CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor, CategoryTheory.Limits.Trident.app_zero_assoc, CategoryTheory.Limits.PullbackCone.isIso_snd_of_mono_of_isLimit, CategoryTheory.Limits.combineCones_pt_map, toStructuredArrow_comp_proj, CategoryTheory.Abelian.epi_fst_of_isLimit, CategoryTheory.Mon.limit_mon_one, CategoryTheory.Limits.Cofork.op_Ο_app_one, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_auxβ, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp_assoc, CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.IsLimit.map_Ο_assoc, mapConeToUnder_hom_hom, LightProfinite.Extend.functor_initial, functoriality_map_hom, CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift, ModuleCat.HasLimit.productLimitCone_cone_pt_isAddCommGroup, CategoryTheory.Limits.BinaryFan.leftUnitor_inv, postcomposeId_inv_app_hom, CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc, CategoryTheory.Functor.mapConeOp_hom_hom, CategoryTheory.coherentTopology.isLocallySurjective_Ο_app_zero_of_isLocallySurjective_map, CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst_assoc, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, CategoryTheory.Limits.KernelFork.map_ΞΉ, ModuleCat.binaryProductLimitCone_cone_pt, CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_map, CategoryTheory.Limits.equalizer.fork_Ο_app_zero, CategoryTheory.Comma.coneOfPreserves_pt_left, CategoryTheory.Functor.structuredArrowMapCone_pt, CommGrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Limits.coneOfConeUncurry_pt, CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction, CategoryTheory.Limits.Multifork.hom_comp_ΞΉ, CategoryTheory.Limits.coconeOpEquiv_counitIso, w_apply, CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, overPost_Ο_app, toStructuredArrow_map, CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom, CategoryTheory.Limits.PushoutCocone.unop_pt, CategoryTheory.Limits.Multifork.pi_condition_assoc, CategoryTheory.Limits.SequentialProduct.cone_Ο_app, CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom, CategoryTheory.Limits.limit.lift_Ο_app_assoc, w_assoc, extendComp_hom_hom, AlgebraicGeometry.isAffineHom_Ο_app, LightProfinite.Extend.functor_obj, CategoryTheory.Limits.coconeLeftOpOfConeEquiv_counitIso, CategoryTheory.Limits.Multifork.ext_inv_hom, CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left, op_pt, CategoryTheory.ShortComplex.exact_iff_of_forks, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff, CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_Ο_app_f, CategoryTheory.Limits.combineCones_pt_obj, CategoryTheory.Limits.coconeRightOpOfCone_pt, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_snd, CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_Ο_app, CategoryTheory.Functor.mapConeMapCone_inv_hom, CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac, CategoryTheory.Limits.IsLimit.homEquiv_symm_naturality, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff', CategoryTheory.Limits.BinaryFan.ext_hom_hom, CategoryTheory.Functor.IsEventuallyConstantTo.isIso_Ο_of_isLimit', LightProfinite.instEpiAppOppositeNatΟAsLimitCone, CategoryTheory.FunctorToTypes.binaryProductCone_pt_map, CategoryTheory.Limits.IsLimit.pushout_hom_ext, CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd_assoc, CategoryTheory.Limits.IsLimit.isZero_pt, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.Ο_comp_isoHomology_hom, CategoryTheory.Limits.BinaryFan.assocInv_snd, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.Limits.PullbackCone.isoMk_hom_hom, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.Limits.Multifork.ofPiFork_ΞΉ, CategoryTheory.Functor.Initial.extendCone_obj_Ο_app, CategoryTheory.Limits.Fork.condition_assoc, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp, CategoryTheory.Limits.Cocone.unop_pt, CategoryTheory.preserves_lift_mapCone, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, extendIso_inv_hom, CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom, CategoryTheory.Limits.Wedge.condition_assoc, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, CategoryTheory.Limits.coconeUnopOfCone_ΞΉ, CategoryTheory.Limits.BinaryFan.assocInv_fst, CategoryTheory.Limits.Fork.isoForkOfΞΉ_inv_hom, CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj_assoc, postcomposeId_hom_app_hom, CategoryTheory.Limits.BinaryFan.Ο_app_left, CategoryTheory.Functor.mapConeWhisker_inv_hom, CategoryTheory.Limits.IsLimit.existsUnique, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ΞΉ_assoc, toStructuredArrowCompToUnderCompForget_inv_app, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_H, CategoryTheory.mono_iff_isIso_fst, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_Ο_app_walkingParallelPair_zero, CategoryTheory.WithTerminal.coneEquiv_functor_obj_pt, CategoryTheory.Limits.IsLimit.homIso_hom, CategoryTheory.Limits.PullbackCone.ofCone_pt, CategoryTheory.liftedLimitMapsToOriginal_hom_Ο, CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.rightUnitor_naturality, CategoryTheory.Limits.PullbackCone.mk_Ο_app_left, CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone, TopCat.isSheaf_of_isLimit, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe, extensions_app, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso, CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_Ο_app, CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc, AddGrpCat.binaryProductLimitCone_cone_pt, CategoryTheory.Limits.coneOfIsSplitMono_pt, CommRingCat.prodFan_pt, TopCat.Sheaf.interUnionPullbackCone_pt, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv, Profinite.exists_locallyConstant_finite_nonempty, CategoryTheory.Limits.BinaryFan.assoc_fst, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.Limits.limit.lift_map_assoc, CategoryTheory.Limits.Types.Limit.lift_Ο_apply', CategoryTheory.mono_iff_isIso_snd, AddCommGrpCat.binaryProductLimitCone_cone_Ο_app_right, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, CategoryTheory.PreOneHypercover.forkOfIsColimit_ΞΉ_map_inj, CategoryTheory.PreservesFiniteLimitsOfFlat.fac, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit_lift_f, CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_neg, CategoryTheory.IsPullback.of_isLimit_cone, CategoryTheory.Limits.limit.lift_Ο, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ΞΉ, CategoryTheory.Limits.wideEqualizer.trident_Ο_app_zero, CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd, CategoryTheory.Limits.Multifork.hom_comp_ΞΉ_assoc, CategoryTheory.Limits.Bicone.ofLimitCone_pt, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.Ο_comp_isoHomology_hom_assoc, CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map, Profinite.exists_locallyConstant_fin_two, PresheafOfModules.limitCone_pt, Profinite.Extend.functor_initial, CategoryTheory.Over.liftCone_pt, toStructuredArrowCone_pt, CategoryTheory.Abelian.AbelianStruct.ΞΉ_imageΟ, CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, CategoryTheory.Limits.Multifork.app_right_eq_ΞΉ_comp_fst, CommRingCat.instIsLocalHomCarrierPtWalkingParallelPairEqualizerForkRingHomHomΞΉ, HomologicalComplex.isIso_Ο_f_of_isLimit_of_isEventuallyConstantTo, postcompose_map_hom, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForgetβContinuousMonoidHomToProfiniteContinuousMap, eta_inv_hom, CategoryTheory.Limits.BinaryFan.mk_pt, Profinite.Extend.functor_map, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom_assoc, CategoryTheory.Limits.BinaryBicone.ofLimitCone_pt, CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, CategoryTheory.Limits.Trident.IsLimit.homIso_natural, CategoryTheory.ObjectProperty.prop_of_isLimit_binaryFan, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc, CategoryTheory.Limits.Multifork.toPiFork_Ο_app_zero, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom, CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone, CategoryTheory.Limits.Types.surjective_Ο_app_zero_of_surjective_map_aux, CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_f, CategoryTheory.Limits.IsLimit.isIso_Ο_app_of_isInitial, CategoryTheory.Limits.coneOfCoconeUnop_pt, CategoryTheory.Limits.Multifork.toSections_fac, Profinite.isIso_asLimitCone_lift, TopCat.coneOfConeForget_pt, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_fst, CategoryTheory.Limits.Fork.unop_Ο, CategoryTheory.WithTerminal.coneEquiv_counitIso_hom_app_hom, LightProfinite.Extend.functorOp_final, CategoryTheory.Limits.limit.lift_extend, TopCat.isTopologicalBasis_cofiltered_limit, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inr, CategoryTheory.IsPullback.of_is_product, CategoryTheory.Limits.Multifork.isLimit_types_iff, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.Limits.Types.isLimit_iff, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_Ο_app, CategoryTheory.Limits.combineCones_Ο_app_app, CategoryTheory.Limits.instIsIsoHomHomCone, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft, CategoryTheory.Limits.KernelFork.mapOfIsLimit_ΞΉ, CategoryTheory.Limits.Multifork.condition_assoc, Preorder.isGLB_of_isLimit, CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom, Algebra.codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat, CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_Ο, CategoryTheory.Limits.WidePullbackCone.condition, CategoryTheory.Adjunction.functorialityCounit'_app_hom, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_right_as, CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.injective, CategoryTheory.Limits.Fork.app_one_eq_ΞΉ_comp_right, Profinite.exists_hom, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac, CategoryTheory.Limits.coneRightOpOfCoconeEquiv_counitIso, AlgebraicGeometry.Scheme.isAffine_of_isLimit, CategoryTheory.Limits.FormalCoproduct.isPullback, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_pt, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom, CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv_assoc, CompHausLike.pullback.cone_pt, CategoryTheory.Limits.coconeLeftOpOfCone_pt, CategoryTheory.Limits.ConeMorphism.inv_hom_id, CategoryTheory.Limits.Fork.equalizer_ext, CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ΞΉ, CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac, op_ΞΉ, CategoryTheory.WithTerminal.coneEquiv_functor_map_hom, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, CategoryTheory.Limits.IsLimit.homEquiv_apply, CategoryTheory.Limits.CompleteLattice.limitCone_cone_pt, CategoryTheory.Limits.Multifork.pi_condition, CategoryTheory.Limits.KernelFork.map_condition_assoc, CategoryTheory.Comma.coneOfPreserves_Ο_app_left
|
unop π | CompOp | 5 mathmath: unop_ΞΉ, CategoryTheory.Limits.coconeOpEquiv_inverse_map, CategoryTheory.Limits.coconeOpEquiv_inverse_obj, unop_pt, CategoryTheory.Limits.coconeOpEquiv_counitIso
|
whisker π | CompOp | 16 mathmath: whisker_Ο, CategoryTheory.Functor.Initial.limitConeComp_isLimit, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, whiskering_map_hom, CategoryTheory.Functor.Initial.limitConeComp_cone, CategoryTheory.Limits.PushoutCocone.op_Ο_app, CategoryTheory.Limits.PullbackCone.unop_ΞΉ_app, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, CategoryTheory.Limits.limit.lift_pre, CategoryTheory.Functor.mapConeWhisker_hom_hom, CategoryTheory.Limits.limit.pre_eq, whiskering_obj, whisker_pt, equivalenceOfReindexing_counitIso, equivalenceOfReindexing_unitIso, CategoryTheory.Functor.mapConeWhisker_inv_hom
|
whiskering π | CompOp | 15 mathmath: whiskeringEquivalence_functor, CategoryTheory.Functor.Initial.conesEquiv_counitIso, CategoryTheory.Over.conePostIso_hom_app_hom, whiskeringEquivalence_unitIso, whiskering_map_hom, CategoryTheory.Functor.Initial.conesEquiv_unitIso, CategoryTheory.Functor.Initial.conesEquiv_inverse, equivalenceOfReindexing_functor, whiskeringEquivalence_counitIso, CategoryTheory.Over.conePostIso_inv_app_hom, whiskering_obj, equivalenceOfReindexing_counitIso, equivalenceOfReindexing_unitIso, equivalenceOfReindexing_inverse, whiskeringEquivalence_inverse
|
whiskeringEquivalence π | CompOp | 4 mathmath: whiskeringEquivalence_functor, whiskeringEquivalence_unitIso, whiskeringEquivalence_counitIso, whiskeringEquivalence_inverse
|
Ο π | CompOp | 329 mathmath: CategoryTheory.Limits.limitConeOfUnique_cone_Ο, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac, LightProfinite.Extend.functorOp_obj, CategoryTheory.Limits.Trident.app_zero, AlgebraicGeometry.opensCone_pt, unop_ΞΉ, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, ofTrident_Ο, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_Ο_app, CategoryTheory.Comonad.ComonadicityInternal.unitFork_Ο_app, CategoryTheory.Limits.pullbackConeOfLeftIso_Ο_app_left, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc, CategoryTheory.Functor.isLimitConeOfIsRightKanExtension_lift, CategoryTheory.Limits.Pi.cone_Ο, Profinite.Extend.functorOp_map, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, CategoryTheory.Limits.BinaryBicone.toCone_Ο_app_right, CategoryTheory.Limits.IsLimit.map_Ο, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_Ο_app_f, CategoryTheory.Limits.PullbackCone.Ο_app_right, CategoryTheory.Limits.PushoutCocone.unop_Ο_app, CategoryTheory.Limits.Fork.unop_ΞΉ_app_zero, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_pos_assoc, Profinite.Extend.cone_Ο_app, CategoryTheory.Limits.Cocone.unop_Ο, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_Ο_app_left, CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.fac, eta_hom_hom, toCostructuredArrow_obj, CategoryTheory.Functor.IsEventuallyConstantTo.cone_Ο_app, CategoryTheory.Comma.coneOfPreserves_Ο_app_right, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_Ο_app_walkingParallelPair_one, CategoryTheory.Functor.RightExtension.coneAt_Ο_app, CategoryTheory.Limits.coneOfDiagramTerminal_Ο_app, whisker_Ο, CategoryTheory.Under.liftCone_pt, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsColimit_inv_comp_map_Ο, CategoryTheory.Limits.PullbackCone.mk_Ο_app, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp, CategoryTheory.Over.conePost_obj_Ο_app, ModuleCat.HasLimit.productLimitCone_cone_Ο, CategoryTheory.Limits.Cofork.unop_Ο_app_one, fromStructuredArrow_Ο_app, CategoryTheory.Limits.pullbackConeOfLeftIso_Ο_app_right, Profinite.exists_locallyConstant_finite_aux, fromCostructuredArrow_obj_Ο, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.ProdPreservesConnectedLimits.forgetCone_Ο, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_Ο_app, CategoryTheory.Limits.ConeMorphism.w, extend_Ο, CategoryTheory.Limits.Bicone.toCone_Ο_app_mk, CategoryTheory.Limits.coneOfCoconeRightOp_Ο, CategoryTheory.Limits.BinaryBicone.toCone_Ο_app_left, CategoryTheory.WithTerminal.coneEquiv_functor_obj_Ο_app_star, Profinite.Extend.functorOp_obj, CategoryTheory.Limits.coneOfDiagramInitial_Ο_app, CategoryTheory.Limits.WidePullbackShape.mkCone_Ο_app, CategoryTheory.Monad.ForgetCreatesLimits.newCone_Ο_app, ModuleCat.binaryProductLimitCone_cone_Ο_app_right, CategoryTheory.Limits.PullbackCone.combine_Ο_app, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_Ο_app_coe, LightProfinite.lightToProfinite_map_proj_eq, CategoryTheory.Limits.Multiequalizer.multifork_Ο_app_left, CategoryTheory.Cat.HasLimits.limitCone_Ο_app, CategoryTheory.Limits.ConeMorphism.map_w_assoc, CategoryTheory.Limits.limit.isoLimitCone_hom_Ο_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_Ο_app, AlgebraicGeometry.isBasis_preimage_isAffineOpen, CategoryTheory.Limits.PullbackCone.op_ΞΉ_app, CategoryTheory.Limits.Fork.unop_ΞΉ_app_one, CategoryTheory.Functor.Initial.extendCone_obj_Ο_app', CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom_Ο_app, CategoryTheory.Mon.limit_mon_mul, AddCommGrpCat.binaryProductLimitCone_cone_Ο_app_left, CategoryTheory.Limits.coneOfCoconeLeftOp_Ο_app, CategoryTheory.Limits.coneOfCoconeUnop_Ο, PresheafOfModules.limitCone_Ο_app_app, CategoryTheory.Limits.Types.isLimitEquivSections_apply, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_neg_assoc, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_Ο_app_eq_sum, CategoryTheory.Limits.coneOfIsSplitMono_Ο_app, CategoryTheory.WithTerminal.coneEquiv_functor_obj_Ο_app_of, CategoryTheory.Limits.IsLimit.homEquiv_symm_Ο_app, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, TopCat.nonempty_isLimit_iff_eq_induced, ofPullbackCone_Ο, AlgebraicGeometry.exists_appTop_Ο_eq_of_isAffine_of_isLimit, CategoryTheory.Limits.ConeMorphism.map_w, CategoryTheory.Limits.limit.isoLimitCone_hom_Ο, CategoryTheory.Limits.pullbackConeOfRightIso_Ο_app_right, CategoryTheory.Limits.Fork.ofΞΉ_Ο_app, CategoryTheory.Limits.IsLimit.hom_lift, CategoryTheory.Limits.PullbackCone.mk_Ο_app_right, CategoryTheory.Limits.Cofork.op_Ο_app_zero, CategoryTheory.Limits.coneOfConeCurry_Ο_app, CategoryTheory.Limits.Types.limitCone_Ο_app, postcompose_obj_Ο, toStructuredArrowCone_Ο_app, Condensed.isColimitLocallyConstantPresheaf_desc_apply, Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceΟAsLimitCone, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsLimit_hom_comp_Ο, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp_assoc, CategoryTheory.Limits.PullbackCone.mk_Ο_app_one, LightProfinite.Extend.functor_map, CategoryTheory.Over.conePost_map_hom, CategoryTheory.Limits.Fork.ofCone_Ο, AlgebraicGeometry.exists_preimage_eq, CategoryTheory.Limits.Types.limitConeIsLimit_lift_coe, Profinite.exists_isClopen_of_cofiltered, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc, CategoryTheory.Limits.coneRightOpOfCocone_Ο, CategoryTheory.Limits.Multifork.app_right_eq_ΞΉ_comp_snd, CategoryTheory.Limits.PullbackCone.Ο_app_left, CategoryTheory.Limits.Multifork.app_left_eq_ΞΉ, CategoryTheory.Limits.coconeOfConeRightOp_ΞΉ, CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp_assoc, CategoryTheory.Under.liftCone_Ο_app, CategoryTheory.Limits.Fork.app_one_eq_ΞΉ_comp_left, CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_pt, CategoryTheory.Mon.limitCone_Ο_app_hom, CategoryTheory.Comma.limitAuxiliaryCone_Ο_app, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_hom, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsColimit_inv_comp_map_Ο_assoc, Profinite.Extend.functor_obj, CategoryTheory.Functor.Initial.extendCone_map_hom, toCostructuredArrow_map, CategoryTheory.Limits.BinaryFan.Ο_app_right, AlgebraicGeometry.opensCone_Ο_app, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_auxβ, CategoryTheory.Limits.PushoutCocone.op_Ο_app, CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_Ο, CategoryTheory.Limits.limit.lift_Ο_app, equiv_inv_Ο, CategoryTheory.biconeMk_map, CategoryTheory.Limits.Types.Small.limitCone_Ο_app, CategoryTheory.Limits.Fork.app_one_eq_ΞΉ_comp_right_assoc, overPost_pt, CategoryTheory.Functor.Initial.limit_cone_comp_aux, CategoryTheory.Over.liftCone_Ο_app, CategoryTheory.Limits.isLimitConeOfAdj_lift, CategoryTheory.Limits.Types.Limit.lift_Ο_apply, equiv_hom_snd, functoriality_obj_Ο_app, CategoryTheory.Limits.ConeMorphism.w_assoc, CategoryTheory.Limits.PullbackCone.unop_ΞΉ_app, CategoryTheory.Limits.Multifork.toPiFork_Ο_app_one, CategoryTheory.Limits.pullbackConeOfLeftIso_Ο_app_none, CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit, CategoryTheory.Limits.PullbackCone.isoMk_inv_hom, AddCommGrpCat.HasLimit.productLimitCone_cone_Ο, CategoryTheory.Limits.limit.isoLimitCone_inv_Ο_assoc, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_auxβ, CategoryTheory.Functor.mapConeβ_Ο_app, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_pos, CategoryTheory.Limits.PreservesLimitβ.isoObjConePointsOfIsLimit_hom_comp_Ο_assoc, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_Ο_app, LightProfinite.Extend.functorOp_map, Alexandrov.lowerCone_Ο_app, CategoryTheory.Limits.coneLeftOpOfCocone_Ο_app, ModuleCat.binaryProductLimitCone_cone_Ο_app_left, CategoryTheory.liftedLimitMapsToOriginal_inv_map_Ο, CategoryTheory.Limits.KernelFork.app_one, CategoryTheory.Functor.coneOfIsRightKanExtension_Ο, CategoryTheory.Limits.Fork.app_zero_eq_ΞΉ, CategoryTheory.Limits.limit.cone_Ο, CategoryTheory.Limits.IsLimit.isIso_limMap_Ο, CategoryTheory.Limits.limit.lift_Ο_apply, CategoryTheory.Limits.pullbackConeOfRightIso_Ο_app_left, ProfiniteGrp.cone_Ο_app, CategoryTheory.Limits.Trident.ofCone_Ο, CompHausLike.pullback.cone_Ο, CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Functor.mapCone_Ο_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_Ο_app, CategoryTheory.Sheaf.coneΞ_Ο_app, CategoryTheory.Limits.coneOfConeUncurry_Ο_app, CategoryTheory.Limits.asEmptyCone_Ο_app, CategoryTheory.Limits.Fork.op_ΞΉ_app, CategoryTheory.Functor.IsEventuallyConstantTo.isIso_Ο_of_isLimit, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_Ο_app, CategoryTheory.Limits.Trident.ofΞΉ_Ο_app, CategoryTheory.Limits.coneOfSectionCompYoneda_Ο, CategoryTheory.Limits.Concrete.surjective_Ο_app_zero_of_surjective_map, Profinite.exists_locallyConstant, CategoryTheory.Limits.Trident.equalizer_ext, CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_Ο_app, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.extendFan_Ο_app, CategoryTheory.Limits.BinaryBicone.ofLimitCone_snd, CategoryTheory.Over.conePost_obj_pt, CategoryTheory.Limits.limitConeOfUnique_isLimit_lift, CategoryTheory.coherentTopology.epi_Ο_app_zero_of_epi, CategoryTheory.Limits.Trident.ΞΉ_eq_app_zero, CategoryTheory.Limits.Fork.op_ΞΉ_app_one, w, CategoryTheory.Limits.PullbackCone.ofCone_Ο, AlgebraicGeometry.ExistsHomHomCompEqCompAux.hab, CategoryTheory.Limits.Cofork.unop_Ο_app_zero, toStructuredArrow_obj, CategoryTheory.Limits.IsLimit.fac_assoc, CategoryTheory.Limits.IsLimit.homEquiv_symm_Ο_app_assoc, CategoryTheory.Limits.limit.homIso_hom, TopCat.coneOfConeForget_Ο_app, CategoryTheory.Limits.Bicone.ofLimitCone_Ο, ofFork_Ο, TopCat.induced_of_isLimit, CategoryTheory.Limits.Types.surjective_Ο_app_zero_of_surjective_map, CategoryTheory.Limits.coconeLeftOpOfCone_ΞΉ_app, AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty', isLimit_iff_isIso_limMap_Ο, CategoryTheory.Limits.coconeRightOpOfCone_ΞΉ, CategoryTheory.Limits.PullbackCone.combine_pt_map, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.PullbackCone.equalizer_ext, CategoryTheory.Limits.Multifork.app_right_eq_ΞΉ_comp_snd_assoc, Preorder.coneOfLowerBound_Ο_app, CategoryTheory.Limits.limit.lift_Ο_assoc, AddCommGrpCat.HasLimit.lift_hom_apply, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_Ο_app, CategoryTheory.Limits.Multifork.ofPiFork_Ο_app_right, LightCondensed.epi_Ο_app_zero_of_epi, AlgebraicGeometry.exists_appTop_Ο_eq_of_isLimit, TopCat.Presheaf.isGluing_iff_pairwise, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_Ο_app, CategoryTheory.Limits.pullbackConeOfRightIso_Ο_app_none, HomologicalComplex.quasiIsoAt_Ο_of_isLimit_of_isEventuallyConstantTo, ModuleCat.HasLimit.lift_hom_apply, CategoryTheory.FunctorToTypes.binaryProductCone_Ο_app, ModuleCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.Limits.Multifork.ofΞΉ_Ο_app, CategoryTheory.Limits.limit.isoLimitCone_inv_Ο, CategoryTheory.Limits.Bicone.toCone_Ο_app, HomologicalComplex.coneOfHasLimitEval_Ο_app_f, CategoryTheory.Subobject.leInfCone_Ο_app_none, CategoryTheory.Limits.PullbackCone.condition_one, CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_Ο_app, CategoryTheory.Limits.BinaryBicone.ofLimitCone_fst, toUnder_Ο_app, CategoryTheory.Limits.coneOfSectionCompCoyoneda_Ο, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp_assoc, CategoryTheory.Limits.coconeOfConeLeftOp_ΞΉ_app, CategoryTheory.Limits.limit.coneMorphism_Ο, CategoryTheory.Limits.Cocone.op_Ο, CategoryTheory.Limits.coconeOfConeUnop_ΞΉ, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty, CategoryTheory.Limits.Fork.op_ΞΉ_app_zero, AlgebraicGeometry.Scheme.exists_Ο_app_comp_eq_of_locallyOfFinitePresentation, CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor, CategoryTheory.Limits.Trident.app_zero_assoc, CategoryTheory.Limits.combineCones_pt_map, CategoryTheory.Limits.Cofork.op_Ο_app_one, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_auxβ, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp_assoc, CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.IsLimit.map_Ο_assoc, functoriality_map_hom, CategoryTheory.coherentTopology.isLocallySurjective_Ο_app_zero_of_isLocallySurjective_map, CategoryTheory.Limits.equalizer.fork_Ο_app_zero, w_apply, overPost_Ο_app, toStructuredArrow_map, CategoryTheory.Limits.SequentialProduct.cone_Ο_app, CategoryTheory.Limits.limit.lift_Ο_app_assoc, w_assoc, AlgebraicGeometry.isAffineHom_Ο_app, LightProfinite.Extend.functor_obj, CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left, CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_Ο_app_f, CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_Ο_app, CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac, CategoryTheory.Limits.CompleteLattice.limitCone_cone_Ο_app, CategoryTheory.Functor.IsEventuallyConstantTo.isIso_Ο_of_isLimit', LightProfinite.instEpiAppOppositeNatΟAsLimitCone, CategoryTheory.Limits.PullbackCone.isoMk_hom_hom, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.Functor.Initial.extendCone_obj_Ο_app, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp, CategoryTheory.Limits.coconeUnopOfCone_ΞΉ, CategoryTheory.Limits.BinaryFan.Ο_app_left, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_Ο_app_walkingParallelPair_zero, CategoryTheory.Limits.IsLimit.homIso_hom, CategoryTheory.liftedLimitMapsToOriginal_hom_Ο, CategoryTheory.Limits.PullbackCone.mk_Ο_app_left, extensions_app, CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_Ο_app, CategoryTheory.Limits.coneUnopOfCocone_Ο, Profinite.exists_locallyConstant_finite_nonempty, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_Ο_app, CategoryTheory.Limits.Types.Limit.lift_Ο_apply', AddCommGrpCat.binaryProductLimitCone_cone_Ο_app_right, CategoryTheory.PreservesFiniteLimitsOfFlat.fac, CategoryTheory.Limits.constCone_Ο, CategoryTheory.Limits.SequentialProduct.cone_Ο_app_comp_Pi_Ο_neg, CategoryTheory.IsPullback.of_isLimit_cone, CategoryTheory.Limits.limit.lift_Ο, CategoryTheory.Limits.wideEqualizer.trident_Ο_app_zero, Profinite.exists_locallyConstant_fin_two, CategoryTheory.Comonad.beckCoalgebraFork_Ο_app, TopCat.piFan_Ο_app, CategoryTheory.Limits.Fan.mk_Ο_app, CategoryTheory.Limits.Multifork.app_right_eq_ΞΉ_comp_fst, HomologicalComplex.isIso_Ο_f_of_isLimit_of_isEventuallyConstantTo, postcompose_map_hom, eta_inv_hom, Profinite.Extend.functor_map, CategoryTheory.Limits.coneOfAdj_Ο, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, CategoryTheory.Under.forgetCone_Ο_app, CategoryTheory.Limits.Types.surjective_Ο_app_zero_of_surjective_map_aux, CategoryTheory.Limits.IsLimit.isIso_Ο_app_of_isInitial, TopCat.isTopologicalBasis_cofiltered_limit, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_Ο_app, CategoryTheory.Limits.combineCones_Ο_app_app, CategoryTheory.Limits.Fork.app_one_eq_ΞΉ_comp_right, Profinite.exists_hom, CategoryTheory.Limits.Fork.equalizer_ext, CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply, op_ΞΉ, CategoryTheory.WithTerminal.coneEquiv_functor_map_hom, CategoryTheory.Functor.structuredArrowMapCone_Ο_app, CategoryTheory.Limits.IsLimit.homEquiv_apply, CategoryTheory.Comma.coneOfPreserves_Ο_app_left
|