| Metric | Count |
|---|
DefinitionsColimitCocone, cocone, isColimit, HasColimit, isoOfEquivalence, isoOfNatIso, HasColimitsOfShape, HasColimitsOfSize, HasLimit, isoOfEquivalence, isoOfNatIso, HasLimits, HasLimitsOfShape, HasLimitsOfSize, op, unop, op, unop, LimitCone, cone, isLimit, colim, colimConstAdj, colimCoyoneda, colimMap, colimit, cocone, coconeMorphism, desc, homIso, homIso', isColimit, isoColimitCocone, post, pre, ι, coneOfAdj, constLimAdj, getColimitCocone, getLimitCone, isColimitEquivIsLimitOp, isColimitOfOp, isColimitOfUnop, isLimitConeOfAdj, isLimitEquivIsColimitOp, isLimitOfOp, isLimitOfUnop, lim, limMap, limYoneda, limit, cone, coneMorphism, homIso, homIso', isLimit, isoLimitCone, post, pre, π | 60 |
Theoremsexists_colimit, isoOfEquivalence_hom_π, isoOfEquivalence_inv_π, isoOfNatIso_hom_desc, isoOfNatIso_hom_desc_assoc, isoOfNatIso_inv_desc, isoOfNatIso_inv_desc_assoc, isoOfNatIso_ι_hom, isoOfNatIso_ι_hom_assoc, isoOfNatIso_ι_inv, isoOfNatIso_ι_inv_assoc, mk, ofCoconesIso, hasColimitsOfShape, has_colimit, of_essentiallySmall, of_small, has_colimits_of_shape, exists_limit, isoOfEquivalence_hom_π, isoOfEquivalence_inv_π, isoOfNatIso_hom_π, isoOfNatIso_hom_π_assoc, isoOfNatIso_inv_π, isoOfNatIso_inv_π_assoc, lift_isoOfNatIso_hom, lift_isoOfNatIso_hom_assoc, lift_isoOfNatIso_inv, lift_isoOfNatIso_inv_assoc, mk, ofConesIso, has_limits_of_shape, has_limit, of_essentiallySmall, of_small, has_limits_of_shape, colimMap_epi, colimMap_epi', colimMap_eq, colim_map, colim_obj, coconeMorphism_hom, cocone_x, cocone_ι, comp_coconePointUniqueUpToIso_hom, comp_coconePointUniqueUpToIso_hom_assoc, comp_coconePointUniqueUpToIso_inv, comp_coconePointUniqueUpToIso_inv_assoc, desc_cocone, desc_extend, eqToHom_comp_ι, eqToHom_comp_ι_assoc, existsUnique, homIso_hom, hom_ext, hom_ext_iff, isColimit_desc, isoColimitCocone_ι_hom, isoColimitCocone_ι_hom_assoc, isoColimitCocone_ι_inv, isoColimitCocone_ι_inv_assoc, map_desc, map_desc_assoc, map_post, post_desc, post_post, pre_desc, pre_desc_assoc, pre_eq, pre_id, pre_map, pre_map', pre_post, pre_pre, w, w_assoc, ι_coconeMorphism, ι_desc, ι_desc_assoc, ι_inv_pre, ι_inv_pre_assoc, ι_map, ι_map_assoc, ι_post, ι_post_assoc, ι_pre, ι_pre_assoc, coneOfAdj_pt, coneOfAdj_π, hasColimitOfHasColimitsOfShape, hasColimit_equivalence_comp, hasColimit_iff_of_iso, hasColimit_of_equivalence_comp, hasColimit_of_iso, hasColimitsOfShapeOfHasColimitsOfSize, hasColimitsOfShape_of_equivalence, hasColimitsOfSizeOfUnivLE, hasColimitsOfSizeShrink, hasLimitOfHasLimitsOfShape, hasLimit_equivalence_comp, hasLimit_iff_of_iso, hasLimit_of_equivalence_comp, hasLimit_of_iso, hasLimitsOfShapeOfHasLimits, hasLimitsOfShape_of_equivalence, hasLimitsOfSizeOfUnivLE, hasLimitsOfSizeShrink, hasSmallestColimitsOfHasColimits, hasSmallestLimitsOfHasLimits, instIsLeftAdjointFunctorColim, instIsRightAdjointFunctorLim, isLimitConeOfAdj_lift, limMap_eq, limMap_mono, limMap_mono', limMap_π, limMap_π_assoc, lim_map, lim_obj, coneMorphism_hom, coneMorphism_π, conePointUniqueUpToIso_hom_comp, conePointUniqueUpToIso_hom_comp_assoc, conePointUniqueUpToIso_inv_comp, conePointUniqueUpToIso_inv_comp_assoc, cone_x, cone_π, existsUnique, homIso_hom, hom_ext, hom_ext_iff, id_pre, isLimit_lift, isoLimitCone_hom_π, isoLimitCone_hom_π_assoc, isoLimitCone_inv_π, isoLimitCone_inv_π_assoc, lift_cone, lift_extend, lift_map, lift_map_assoc, lift_post, lift_pre, lift_π, lift_π_assoc, map_post, map_pre, map_pre', post_post, post_π, post_π_assoc, pre_eq, pre_post, pre_pre, pre_π, pre_π_assoc, w, w_assoc, π_comp_eqToHom, π_comp_eqToHom_assoc, ι_colimMap, ι_colimMap_assoc | 162 |
| Total | 222 |
| Name | Category | Theorems |
|---|
ColimitCocone 📖 | CompData | 2 mathmath: CategoryTheory.Presieve.piComparison_fac, HasColimit.exists_colimit
|
HasColimit 📖 | CompData | 80 mathmath: hasColimit_of_equivalence_comp, CategoryTheory.comp_comparison_hasColimit, CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj, hasColimit_iff_of_iso, hasColimitOfHasColimitsOfShape, CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves, AlgebraicGeometry.instHasColimitOverSchemeTopMorphismProperty, Preorder.hasColimit_iff_hasLUB, ModuleCat.HasColimit.instHasColimit, instHasColimitProd, AddCommGrpCat.hasColimit_of_small_quot, hasColimitCompEvaluation, hasColimit_of_hasLimit_leftOp, hasColimit_equivalence_comp, CategoryTheory.comp_comparison_forget_hasColimit, CategoryTheory.Functor.Final.hasColimit_of_comp, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair, Types.instHasColimitConstPUnitFunctor, instHasColimitObjFunctorConstInitial, CategoryTheory.Functor.Final.hasColimit_comp_iff, hasColimit_of_domain_hasInitial, hasReflexiveCoequalizer_iff_hasCoequalizer, ofIsReflexivePair_hasColimit_of_hasCoequalizer, CategoryTheory.Comma.hasColimit, CategoryTheory.IsFiltered.instHasColimitOfIsEventuallyConstant, hasColimit_of_iso, instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor, HasColimit.mk, PartOrdEmb.Limits.instHasColimit, AddCommGrpCat.hasColimit, CategoryTheory.Arrow.hasColimit, CategoryTheory.hasColimit_of_coreflective, CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA, Types.hasColimit, AlgebraicGeometry.instHasColimitOverScheme, Types.hasColimit_iff_small_colimitType, hasColimit_of_hasLimit_rightOp, TopCat.hasColimit_iff_small_colimitType, CategoryTheory.Over.hasColimit_of_hasColimit_comp_forget, hasColimit_of_domain_hasTerminal, CategoryTheory.Adjunction.hasColimit_of_comp_equivalence, hasColimit_of_hasLimit_unop, hasColimit_leftOp_of_hasLimit, hasColimit_of_coequalizer_and_coproduct, hasInitialChangeDiagram, CategoryTheory.Coyoneda.instHasColimitObjOppositeFunctorTypeCoyoneda, Under.hasColimit_of_hasColimit_liftFromUnder, CategoryTheory.MorphismProperty.Comma.hasColimit_of_closedUnderColimitsOfShape, ColimitPresentation.hasColimit, hasColimit_rightOp_of_hasLimit, CategoryTheory.CostructuredArrow.hasColimit, HasColimit.ofCoconesIso, CategoryTheory.NormalEpiCategory.hasColimit_parallelPair, instHasColimitCompOfPreservesColimit, hasColimit_iff_hasInitial_cocone, CategoryTheory.GlueData.hasColimit_multispan_comp, CategoryTheory.PreGaloisCategory.PointedGaloisObject.instHasColimitOppositeFunctorTypeCompOpInclCoyoneda, localCohomology.hasColimitDiagram, instHasColimitOppositeDiscreteOpFunctor, TopModuleCat.instHasColimitOfModuleCatCompForget₂ContinuousLinearMapIdCarrierLinearMap, CategoryTheory.ShortComplex.hasColimit_of_hasColimitπ, CategoryTheory.Adjunction.hasColimit_comp_equivalence, hasColimit_unop_of_hasLimit, CategoryTheory.Functor.Final.comp_hasColimit, hasColimit_const_of_isConnected, HomologicalComplex.instHasColimitDiscreteWalkingPairCompPairEval, CategoryTheory.NormalEpiCategory.pushout_of_epi, hasColimit_of_closedUnderColimits, HasBinaryBiproduct.hasColimit_pair, HasColimitsOfShape.has_colimit, instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂, CategoryTheory.hasColimit_of_created, reflexivePair_hasColimit_of_hasCoequalizer, AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit, AddCommGrpCat.hasColimit_iff_small_quot, CategoryTheory.Functor.IsEventuallyConstantFrom.hasColimit, hasColimit_of_hasLimit_op, CategoryTheory.Comonad.hasColimit_of_comp_forget_hasColimit, hasColimit_op_of_hasLimit
|
HasColimitsOfShape 📖 | CompData | 79 mathmath: hasColimitsOfShape_skeleton, Types.hasColimitsOfShape, CategoryTheory.CosimplicialObject.instHasColimitsOfShape, hasColimitsOfShape_thinSkeleton, FGModuleCat.instHasColimitsOfShapeOfFinCategory, TopCat.instHasColimitsOfShapePresheaf, CategoryTheory.Comma.hasColimitsOfShape, hasColimitsOfShape_of_essentiallySmall, instHasColimitsOfShapeUnderOfWithInitial, CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence, HasIterationOfShape.hasColimitsOfShape, hasColimitsOfShape_widePushoutShape, hasColimitsOfShape_of_initialSeg, CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite, TopCat.topCat_hasColimitsOfShape, CategoryTheory.instHasColimitsOfShapeWalkingParallelPairInd, CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape, CategoryTheory.Sheaf.instHasColimitsOfShape, hasInitialChangeUniverse, hasColimitsOfShape_discrete, CategoryTheory.Over.instHasColimitsOfShape, CategoryTheory.ShortComplex.hasColimitsOfShape, CategoryTheory.Functor.Final.hasColimitsOfShape_of_final, CategoryTheory.hasColimitsOfShape_of_coreflective, AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape, hasColimitsOfShape_op_of_hasLimitsOfShape, CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape, Action.hasColimitsOfShape, CategoryTheory.PreGaloisCategory.instHasColimitsOfShapeSingleObjOfFinite, hasColimitsOfShape_of_hasLimitsOfShape_op, Preorder.instHasColimitsOfShape, CategoryTheory.hasColimitsOfShape_of_reflective, HasColimits.hasColimitsOfShape, hasColimitsOfShape_of_closedUnderColimits, hasColimitsOfShape_iff_isRightAdjoint_const, PresheafOfModules.hasColimitsOfShape, AlgebraicGeometry.instHasColimitsOfShapeDiscreteSchemeOfSmall, instHasColimitsOfShapeOfHasCountableColimitsOfCountableCategory, HasFiniteCoproducts.out, HomologicalComplex.instHasColimitsOfShape, SheafOfModules.instHasColimitsOfShapeOfPresheafOfModulesValRingCat, HasColimitsOfShape.of_essentiallySmall, HasFilteredColimitsOfSize.HasColimitsOfShape, CategoryTheory.OrthogonalReflection.D₂.hasColimitsOfShape, hasReflexiveCoequalizers_iff, CategoryTheory.SimplicialObject.instHasColimitsOfShape, hasColimitsOfShape_of_finallySmall, AlgebraicGeometry.LocallyRingedSpace.instHasColimitsOfShapeDiscrete, CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape, CategoryTheory.GrothendieckTopology.Point.instHasColimitsOfShapeOppositeElementsFiber, hasColimitsOfShape_of_equivalence, hasColimitsOfShape_of_hasFiniteColimits, AddCommGrpCat.hasColimitsOfShape, CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups, PartOrdEmb.Limits.instHasColimitsOfShape, HasColimitsOfShape.of_small, TopModuleCat.instHasColimitsOfShapeOfModuleCat, CategoryTheory.CosimplicialObject.Truncated.instHasColimitsOfShape, HasCountableColimits.out, CategoryTheory.CostructuredArrow.hasColimitsOfShape, hasColimitsOfShape_of_has_filtered_colimits, HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit, hasColimitsOfShape_of_isSuccLimit', functorCategoryHasColimitsOfShape, CategoryTheory.instHasColimitsOfShapeDiscreteIndOfFinite, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, ModuleCat.hasColimitsOfShape, CategoryTheory.SimplicialObject.Truncated.instHasColimitsOfShape, hasColimitsOfShapeOfHasColimitsOfSize, HasColimitsOfSize.has_colimits_of_shape, CategoryTheory.SmallObject.hasColimitsOfShape_discrete, CategoryTheory.Arrow.hasColimitsOfShape, FintypeCat.instHasColimitsOfShapeFintypeCatOfFinCategory, HasFiniteColimits.out, CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite, HasFiniteWidePushouts.out, instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology, AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite, hasColimitsOfShape_of_isSuccLimit
|
HasColimitsOfSize 📖 | CompData | 32 mathmath: Types.hasColimitsOfSize, CategoryTheory.Subobject.hasColimitsOfSize, CategoryTheory.hasColimits_of_reflective, CategoryTheory.MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations, CategoryTheory.IsCardinalLocallyPresentable.toHasColimitsOfSize, CategoryTheory.Comma.hasColimitsOfSize, has_colimits_of_hasCoequalizers_and_coproducts, hasColimitsOfSize_thinSkeleton, instHasColimitsOfSizeUnder, hasColimitsOfSizeOfUnivLE, instHasColimitsOfSizeDiscretePUnit, ModuleCat.hasColimitsOfSize, CategoryTheory.CostructuredArrow.hasColimitsOfSize, TopCat.instHasColimitsOfSizePresheafOfHasColimits, CategoryTheory.hasColimits_of_coreflective, CategoryTheory.hasColimits_of_hasColimits_createsColimits, has_colimits_of_finite_and_filtered, SheafOfModules.instHasColimitsOfSizeOfPresheafOfModulesValRingCat, CategoryTheory.IsGrothendieckAbelian.hasColimits, hasSmallestColimitsOfHasColimits, CompleteLattice.hasColimits_of_completeLattice, CategoryTheory.Sheaf.instHasColimitsOfSize, AddCommGrpCat.hasColimitsOfSize, TopCat.topCat_hasColimitsOfSize, functorCategoryHasColimitsOfSize, CategoryTheory.hasColimitsEssentiallySmallSite, PresheafOfModules.hasColimitsOfSize, hasColimits_op_of_hasLimits, hasColimitsOfSize_skeleton, CategoryTheory.Adjunction.has_colimits_of_equivalence, hasColimits_of_hasLimits_op, hasColimitsOfSizeShrink
|
HasLimit 📖 | CompData | 99 mathmath: CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right', SemiRingCat.hasLimit, hasLimit_iff_hasTerminal_cone, CategoryTheory.hasLimit_of_created, LimitPresentation.hasLimit, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right', CategoryTheory.StructuredArrow.hasLimit, AddCommGrpCat.hasLimit, hasLimit_iff_of_iso, CommGrpCat.hasLimit_iff_small_sections, CategoryTheory.Arrow.hasLimit, hasLimit_leftOp_of_hasColimit, CategoryTheory.comp_comparison_forget_hasLimit, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left', TopModuleCat.hasLimit_of_hasLimit_forget₂, CategoryTheory.Over.hasLimit_of_hasLimit_liftFromOver, CategoryTheory.ShortComplex.hasLimit_of_hasLimitπ, HasBinaryBiproduct.hasLimit_pair, CommRingCat.hasLimit, PresheafOfModules.hasLimit, CategoryTheory.Functor.Initial.hasLimit_comp_iff, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left, ProfiniteGrp.instHasLimit, CategoryTheory.Functor.Initial.comp_hasLimit, hasLimit_of_hasColimit_rightOp, CommSemiRingCat.hasLimit, CategoryTheory.NormalMonoCategory.hasLimit_parallelPair, instHasLimitProd, hasLimit_of_hasColimit_op, hasLimit_of_iso, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right, TopCat.hasLimit_iff_small_sections, ωCPO.instHasLimitWalkingParallelPairParallelPair, Preorder.hasLimit_iff_hasGLB, instHasLimitCompOfPreservesLimit, HomologicalComplex.instHasLimitDiscreteWalkingPairCompPairEval, hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair, hasLimit_of_closedUnderLimits, instHasLimitOppositeDiscreteOpFunctor, CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan, AddGrpCat.hasLimit_iff_small_sections, GrpCat.hasLimit_iff_small_sections, hasLimitOfHasLimitsOfShape, CategoryTheory.Enriched.HasConicalLimit.toHasLimit, CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit, MonCat.HasLimits.hasLimit, hasLimit_unop_of_hasColimit, hasLimit_of_hasColimit_leftOp, CategoryTheory.Adjunction.hasLimit_comp_equivalence, hasLimit_op_of_hasColimit, SemiNormedGrp.hasLimit_parallelPair, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right, Types.hasLimit, instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor, hasLimit_rightOp_of_hasColimit, HasLimit.mk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left, hasTerminalChangeDiagram, CategoryTheory.comp_comparison_hasLimit, hasLimit_of_hasColimit_unop, CompHausLike.instHasLimitWalkingCospanCospan, PresheafOfModules.instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap, hasLimit_of_equivalence_comp, CategoryTheory.NormalMonoCategory.pullback_of_mono, CommMonCat.hasLimit, CategoryTheory.Comonad.forget_creates_limits_of_comonad_preserves, CategoryTheory.Functor.Initial.hasLimit_of_comp, Types.hasLimit_iff_small_sections, CategoryTheory.MonoOver.hasLimit, hasLimitCompEvaluation, CategoryTheory.Comma.hasLimit, HasLimitsOfShape.has_limit, AddGrpCat.hasLimit, hasLimit_const_of_isConnected, RingCat.hasLimit, AddMonCat.HasLimits.hasLimit, HasLimit.ofConesIso, CommGrpCat.hasLimit, ModuleCat.hasLimit, CategoryTheory.Adjunction.hasLimit_of_comp_equivalence, CategoryTheory.Under.hasLimit_of_hasLimit_comp_forget, SheafOfModules.hasLimit, GrpCat.hasLimit, hasLimit_equivalence_comp, hasLimit_of_equalizer_and_product, CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA, instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂, ProfiniteAddGrp.instHasLimit, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left', hasLimit_of_domain_hasTerminal, CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit, instHasLimitObjFunctorConstTerminal, CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape, AddCommGrpCat.hasLimit_iff_small_sections, CategoryTheory.IsCofiltered.instHasLimitOfIsEventuallyConstant, CategoryTheory.hasLimit_of_reflective, hasLimit_of_domain_hasInitial, AddCommMonCat.hasLimit
|
HasLimits 📖 | MathDef | 41 mathmath: AddGrpCat.hasLimits, CategoryTheory.SimplicialObject.Truncated.instHasLimits, ModuleCat.hasLimits', Action.instHasLimits, AlgebraicGeometry.AffineScheme.hasLimits, AddCommGrpCat.hasLimits, AlgebraicGeometry.Scheme.Modules.instHasLimits, instHasLimitsCommAlgCat, CommGrpCat.hasLimits, ModuleCat.hasLimits, CategoryTheory.Arrow.hasLimits, TopCat.topCat_hasLimits, DeltaGenerated.hasLimits, CategoryTheory.instHasLimitsInd, instHasLimitsCondensedMod, instHasLimitsCondensedSet, CommMonCat.hasLimits, CategoryTheory.Cat.instHasLimits, CommRingCat.hasLimits, RingCat.hasLimits, Compactum.instHasLimits, AddMonCat.hasLimits, ωCPO.instHasLimits, hasLimits_of_hasColimits_of_isSeparating, SemiRingCat.hasLimits, CategoryTheory.Under.instHasLimits, CompHaus.hasLimits, CommSemiRingCat.hasLimits, CategoryTheory.CosimplicialObject.Truncated.instHasLimits, CategoryTheory.CosimplicialObject.instHasLimits, SSet.hasLimits, TopModuleCat.instHasLimits, TopCat.instHasLimitsPresheaf, Profinite.hasLimits, AddCommMonCat.hasLimits, CategoryTheory.SimplicialObject.instHasLimits, AlgCat.hasLimits, hasLimits_of_hasColimits_of_hasSeparator, GrpCat.hasLimits, MonCat.hasLimits, SSet.Truncated.hasLimits
|
HasLimitsOfShape 📖 | CompData | 81 mathmath: AddGrpCat.hasLimitsOfShape, CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElements, HasLimitsOfShape.of_small, HasLimitsOfSize.has_limits_of_shape, hasLimitsOfShapeOfHasLimits, CategoryTheory.Under.instHasLimitsOfShape, AddCommGrpCat.hasLimitsOfShape, hasLimitsOfShape_of_closedUnderLimits, HasCofilteredLimitsOfSize.HasLimitsOfShape, CommRingCat.hasLimitsOfShape, hasLimitsOfShape_op_of_hasColimitsOfShape, hasLimitsOfShape_of_hasColimitsOfShape_op, CategoryTheory.CosimplicialObject.instHasLimitsOfShape, RingCat.hasLimitsOfShape, hasLimitsOfShape_iff_isLeftAdjoint_const, CategoryTheory.ShortComplex.hasLimitsOfShape, HasLimits.has_limits_of_shape, hasLimitsOfShape_thinSkeleton, CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence, instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory, CategoryTheory.Subobject.hasLimitsOfShape, TopCat.topCat_hasLimitsOfShape, CategoryTheory.SimplicialObject.instHasLimitsOfShape, CategoryTheory.hasLimitsOfShape_of_coreflective, TopCat.instHasLimitsOfShapePresheaf, CategoryTheory.Arrow.hasLimitsOfShape, Action.hasLimitsOfShape, HomologicalComplex.instHasLimitsOfShape, hasLimitsOfShape_of_initiallySmall, hasLimitsOfShape_widePullbackShape, CategoryTheory.StructuredArrow.hasLimitsOfShape, GrpCat.hasLimitsOfShape, instHasLimitsOfShapeCondensed, CategoryTheory.ShrinkHoms.hasLimitsOfShape, CategoryTheory.CosimplicialObject.Truncated.instHasLimitsOfShape, SemiRingCat.hasLimitsOfShape, CategoryTheory.Enriched.HasConicalLimitsOfShape.hasLimitsOfShape, AddMonCat.HasLimits.hasLimitsOfShape, hasLimitsOfShape_of_equivalence, hasLimitsOfShape_skeleton, CategoryTheory.MonoOver.hasLimitsOfShape, Preorder.instHasLimitsOfShape, CategoryTheory.instHasLimitsOfShapeWalkingParallelPairInd, ModuleCat.hasLimitsOfShape, CategoryTheory.instHasLimitsOfShapeOverOfWithTerminal, CategoryTheory.Comma.hasLimitsOfShape, SheafOfModules.hasLimitsOfShape, MonCat.HasLimits.hasLimitsOfShape, CategoryTheory.Sheaf.instHasLimitsOfShape, functorCategoryHasLimitsOfShape, HasLimitsOfShape.of_essentiallySmall, CategoryTheory.CostructuredArrow.hasLimitsOfShape_of_isConnected, CategoryTheory.SimplicialObject.Truncated.instHasLimitsOfShape, FGModuleCat.instHasLimitsOfShapeOfFinCategory, CategoryTheory.Mon.hasLimitsOfShape, HasCountableLimits.out, CategoryTheory.instHasLimitsOfShapeDiscreteInd, Types.hasLimitsOfShape, FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory, CategoryTheory.hasLimitsOfShape_of_reflective, HasFiniteProducts.out, HasFiniteWidePullbacks.out, TopCat.instHasLimitsOfShapeSheaf, hasTerminalChangeUniverse, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape, hasLimitsOfShape_of_essentiallySmall, TopModuleCat.instHasLimitsOfShapeOfModuleCat, HasFiniteLimits.out, PresheafOfModules.hasLimitsOfShape, hasLimitsOfShape_of_has_cofiltered_limits, AddCommMonCat.hasLimitsOfShape, hasLimitsOfShape_discrete, CategoryTheory.Over.ConstructProducts.over_product_of_widePullback, CategoryTheory.AsSmall.hasLimitsOfShape, CommSemiRingCat.hasLimitsOfShape, CommMonCat.hasLimitsOfShape, CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape, hasLimitsOfShape_of_hasFiniteLimits, CategoryTheory.Functor.Initial.hasLimitsOfShape_of_initial, CategoryTheory.Over.hasLimitsOfShape_of_isConnected, CommGrpCat.hasLimitsOfShape
|
HasLimitsOfSize 📖 | CompData | 53 mathmath: AddMonCat.hasLimitsOfSize, hasLimitsOfSize_skeleton, hasLimitsOfSize_thinSkeleton, SheafOfModules.hasLimitsOfSize, CategoryTheory.instHasLimitsOfSizeOver, AddGrpCat.hasLimitsOfSize, hasLimitsOfSizeOfUnivLE, AddCommGrpCat.hasLimitsOfSize, functorCategoryHasLimitsOfSize, CategoryTheory.IsGrothendieckAbelian.hasLimits, hasLimitsOfSizeShrink, AddCommMonCat.hasLimitsOfSize, CommSemiRingCat.hasLimitsOfSize, CategoryTheory.hasLimitsEssentiallySmallSite, ModuleCat.hasLimitsOfSize, TopCat.topCat_hasLimitsOfSize, CategoryTheory.hasLimits_of_reflective, hasSmallestLimitsOfHasLimits, CommMonCat.hasLimitsOfSize, instHasLimitsOfSizeLightCondSet, CategoryTheory.Adjunction.has_limits_of_equivalence, CompleteLattice.hasLimits_of_completeLattice, Condensed.instHasLimitsOfSizeModuleCat, CommRingCat.hasLimitsOfSize, CategoryTheory.Enriched.HasConicalLimitsOfSize.hasLimitsOfSize, CategoryTheory.hasLimits_of_hasLimits_createsLimits, instHasLimitsOfSizeDiscretePUnit, TopCat.instHasLimitsOfSizeSheafOfHasLimits, hasLimits_of_hasColimits_op, CategoryTheory.StructuredArrow.hasLimitsOfSize, has_limits_of_finite_and_cofiltered, instHasLimitsOfSizeCondensedMod, RingCat.hasLimitsOfSize, CategoryTheory.Comma.hasLimitsOfSize, instHasLimitsOfSizeLightCondMod_1, hasLimits_op_of_hasColimits, MonCat.hasLimitsOfSize, has_limits_of_hasEqualizers_and_products, CategoryTheory.hasLimits_of_coreflective, instHasLimitsOfSizeCondensedSet, GrpCat.hasLimitsOfSize, PresheafOfModules.hasLimitsOfSize, instHasLimitsOfSizeLightCondMod, Types.hasLimitsOfSize, CondensedMod.instHasLimitsOfSizeModuleCat, CommGrpCat.hasLimitsOfSize, CategoryTheory.Sheaf.hasLimitsOfSize, ModuleCat.instHasLimitsOfSize, SemiRingCat.hasLimitsOfSize, CategoryTheory.MonoOver.hasLimitsOfSize, CategoryTheory.Over.hasLimits, CategoryTheory.Subobject.hasLimitsOfSize, AlgCat.hasLimitsOfSize
|
LimitCone 📖 | CompData | 1 mathmath: HasLimit.exists_limit
|
colim 📖 | CompOp | 77 mathmath: colimitIsoFlipCompColim_inv_app, colimitLimitToLimitColimit_isIso, DiagramOfCocones.mkOfHasColimits_coconePoints, colimitUncurryIsoColimitCompColim_ι_ι_inv, CategoryTheory.IsSifted.colim_preservesBinaryProducts_of_isSifted, colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom, colimitIsoSwapCompColim_hom_app, colimit.ι_map, CategoryTheory.IsSifted.factorization_prodComparison_colim, colimitIsoColimitCurryCompColim_ι_hom_assoc, colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv, colimMap_eq, CategoryTheory.IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison, CategoryTheory.Adjunction.colim_preservesColimits, CategoryTheory.preservesColimitNatIso_inv_app, CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits, ι_colimitLimitToLimitColimit_π, colimitUncurryIsoColimitCompColim_ι_hom_assoc, colimitUncurryIsoColimitCompColim_ι_hom, CategoryTheory.IsSifted.colim_preservesLimits_pair_of_sSifted, pointwiseCocone_ι_app_app, colimitIsoColimitCurryCompColim_ι_hom, colimitLimitToLimitColimitCone_hom, pointwiseCocone_pt, colim_map, Types.Colimit.ι_map_apply', colimitIsoColimitCurryCompColim_ι_ι_inv_assoc, CategoryTheory.instPreservesFiniteProductsFunctorColimOfPreadditive, colimitIsoSwapCompColim_inv_app, Types.Colimit.ι_map_apply, CategoryTheory.IsSifted.colim_preservesFiniteProducts_of_isSifted, CategoryTheory.Functor.lanCompColimIso_inv_app, CategoryTheory.preservesColimitNatIso_hom_app, fiberwiseColim_map_app, colimCompFlipIsoWhiskerColim_hom_app_app, DiagramOfCocones.mkOfHasColimits_map_hom, colimit.map_post, colimitFlipIsoCompColim_hom_app, colimIsoFlipCompWhiskerColim_hom_app_app, colim_obj, filtered_colim_preservesFiniteLimits, colimitLimitToLimitColimitCone_iso, instPreservesFiniteLimitsFunctorAddCommGrpCatColim, instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget, instIsLeftAdjointFunctorColim, fiberwiseColimCompEvaluationIso_hom_app, colimit.pre_map', colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc, colimIsoFlipCompWhiskerColim_inv_app_app, colimit.pre_id, colimit.pre_map, colimitIsoFlipCompColim_hom_app, instPreservesHomologyFunctorAddCommGrpCatColim, colimit.ι_map_assoc, fiberwiseColimCompColimIso_hom_app, CategoryTheory.instPreservesLimitsOfShapeFunctorColim, fiberwiseColimCompColimIso_inv_app, ι_colimitLimitToLimitColimit_π_apply, fiberwiseColimCompEvaluationIso_inv_app, CategoryTheory.IsSifted.colim_preservesLimitsOfShape_pempty_of_isSifted, CategoryTheory.IsSifted.colim_preservesTerminal_of_isSifted, colimitIsoColimitCurryCompColim_ι_ι_inv, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc, HasBiproductsOfShape.colimIsoLim_hom_app, isIndObject_limit_comp_yoneda_comp_colim, ι_colimitLimitToLimitColimit_π_assoc, colimCompFlipIsoWhiskerColim_inv_app_app, colimitLimitToLimitColimit_injective, HasBiproductsOfShape.colimIsoLim_inv_app, filtered_colim_preservesFiniteLimits_of_types, colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc, CategoryTheory.Functor.lanCompColimIso_hom_app, instAdditiveFunctorColim, colimitFlipCompColimIsoColimitCompColim_ι_ι_inv, colimitFlipIsoCompColim_inv_app, colimitLimitToLimitColimit_surjective, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom
|
colimConstAdj 📖 | CompOp | — |
colimCoyoneda 📖 | CompOp | — |
colimMap 📖 | CompOp | 36 mathmath: fiberwiseColimit_map, map_π_preserves_coequalizer_inv_colimMap, Bimod.whiskerLeft_hom, colimMap_epi', colimitObjIsoColimitCompEvaluation_inv_colimit_map_assoc, colimitIsoSwapCompColim_hom_app, colimMap_eq, Condensed.lanPresheafExt_inv, colimit.map_desc, map_π_preserves_coequalizer_inv_colimMap_desc, HomologicalComplex.coconeOfHasColimitEval_pt_d, colimitObjIsoColimitCompEvaluation_inv_colimit_map, ι_colimMap, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, IsColimit.isIso_colimMap_ι, ι_colimMap_assoc, colim_map, colimitIsoSwapCompColim_inv_app, map_π_preserves_coequalizer_inv_colimMap_assoc, CategoryTheory.MorphismProperty.colimitsOfShape_colimMap, Cocone.isColimit_iff_isIso_colimMap_ι, PresheafOfModules.colimitPresheafOfModules_map, ModuleCat.HasColimit.coconePointSMul_apply, HomologicalComplex.coconeOfHasColimitEval_ι_app_f, colimit.map_desc_assoc, LightCondensed.lanPresheafExt_inv, Condensed.lanPresheafExt_hom, colimit_map_colimitObjIsoColimitCompEvaluation_hom, colimit_map_colimitObjIsoColimitCompEvaluation_hom_assoc, Bimod.whiskerRight_hom, colimMap_epi, CategoryTheory.MorphismProperty.colimMap, LightCondensed.lanPresheafExt_hom, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, coequalizer.π_colimMap_desc, π_tensor_id_preserves_coequalizer_inv_colimMap_desc
|
colimit 📖 | CompOp | 372 mathmath: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, colimitHomIsoLimitYoneda'_hom_comp_π, smoothSheafCommRing.ι_forgetStalk_inv, IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit, colimitHomIsoLimitYoneda_hom_comp_π, limitUnopIsoUnopColimit_hom_comp_ι, isIso_ι_terminal, CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv_assoc, colimitIsoFlipCompColim_inv_app, colimit.isoColimitCocone_ι_inv, colimitLimitToLimitColimit_isIso, colimitObjIsoColimitCompEvaluation_ι_app_hom_assoc, colimit.eqToHom_comp_ι_assoc, CategoryTheory.ObjectProperty.ColimitOfShape.colimit_toColimitPresentation, fiberwiseColimit_map, colimit.ι_pre_assoc, map_π_preserves_coequalizer_inv_colimMap, ι_comp_colimitOpIsoOpLimit_hom_assoc, HasColimit.isoOfEquivalence_inv_π, ι_colimitCompWhiskeringLeftIsoCompColimit_hom_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, colimit_ι_zero_cokernel_desc_assoc, AlgebraicGeometry.SheafedSpace.colimit_exists_rep, colimitUncurryIsoColimitCompColim_ι_ι_inv, colimit.pre_post, MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom_assoc, smoothSheafCommRing.ι_evalHom_apply, CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, CategoryTheory.ObjectProperty.prop_colimit, colimitCoyonedaHomIsoLimit'_π_apply, colimMap_epi', limitOpIsoOpColimit_hom_comp_ι_assoc, fiberwiseColimit_obj, colimitObjIsoColimitCompEvaluation_ι_inv_assoc, CompleteLattice.colimit_eq_iSup, Sigma.ι_isoColimit_inv, colimitObjIsoColimitCompEvaluation_inv_colimit_map_assoc, colimit.desc_extend, colimit.homIso_hom, ι_colimitPointwiseProductToProductColimit_π, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, Concrete.colimit_rep_eq_iff_exists, colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom, colimitIsoSwapCompColim_hom_app, SingleObj.Types.colimitEquivQuotient_symm_apply, colimit.ι_map, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.PreGaloisCategory.isGalois_iff_aux, colimitIsoColimitCurryCompColim_ι_hom_assoc, PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv_assoc, colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv, CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, colimitYonedaHomIsoLimit'_π_apply, π_comp_colimitLeftOpIsoUnopLimit_inv, CategoryTheory.preservesColimitNatIso_inv_app, colimit.ι_post, colimitHomIsoLimitYoneda'_hom_comp_π_assoc, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, colimit.map_desc, ModuleCat.HasColimit.colimitCocone_ι_app, HasColimit.isoOfEquivalence_hom_π, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, TopCat.colimit_topology, isIso_ι_of_isInitial, HasColimit.isoOfNatIso_ι_inv, fiberwiseColimitLimitIso_hom_app, PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv_assoc, ι_colimitLimitIso_limit_π, CategoryTheory.Functor.Final.ι_colimitIso_hom_assoc, map_π_preserves_coequalizer_inv_colimMap_desc, ι_colimitLimitToLimitColimit_π, π_comp_colimitUnopIsoOpLimit_inv, smoothSheaf.ι_evalHom_assoc, colimit.toOver_ι_app, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion, CategoryTheory.ι_preservesColimitIso_inv_assoc, coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc, colimitObjIsoColimitCompEvaluation_inv_colimit_map, CategoryTheory.Functor.Final.ι_colimitIso_inv, ι_comp_colimitRightOpIsoUnopLimit_hom_assoc, SingleObj.Types.colimitEquivQuotient_apply, CategoryTheory.ι_preservesColimitIso_hom_assoc, ModuleCat.HasColimit.colimitCocone_pt_isModule, CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, colimitUncurryIsoColimitCompColim_ι_hom_assoc, CategoryTheory.Functor.Final.colimitIso_hom, colimit.ι_inv_pre, colimitUncurryIsoColimitCompColim_ι_hom, CategoryTheory.Functor.leftAdjointObjIsDefined_colimit, coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π, CategoryTheory.preservesColimitIso_inv_comp_desc, CategoryTheory.Functor.pointwiseLeftKanExtension_obj, CategoryTheory.Functor.pointwiseLeftKanExtension_map, ι_colimMap, HasColimit.isoOfNatIso_inv_desc_assoc, CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv, π_reflexiveCoequalizerIsoCoequalizer_inv_assoc, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, HasColimit.isoOfNatIso_hom_desc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, IsColimit.isIso_colimMap_ι, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc, IsIPC.isIso, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_f, ι_colimMap_assoc, colimit.ι_pre, colimit.comp_coconePointUniqueUpToIso_inv_assoc, colimitYonedaHomIsoLimit_π_apply, colimitIsoColimitCurryCompColim_ι_hom, colimit.comp_coconePointUniqueUpToIso_hom_assoc, smoothSheafCommRing.ι_evalHom, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, ι_colimitCompWhiskeringLeftIsoCompColimit_hom, CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ι_app, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase_assoc, HomologicalComplex.coconeOfHasColimitEval_pt_X, ι_colimitFiberwiseColimitIso_hom_assoc, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, coconePointwiseProduct_ι_app, π_comp_colimitLeftOpIsoUnopLimit_inv_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, ι_colimitFiberwiseColimitIso_inv_assoc, limitUnopIsoUnopColimit_inv_comp_π_assoc, colimitCoyonedaHomIsoLimitUnop_π_apply, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, colimit.pre_pre, limitRightOpIsoOpColimit_hom_comp_ι, Types.instSubsingletonColimitPUnit, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom_assoc, colimitIsoColimitCurryCompColim_ι_ι_inv_assoc, CategoryTheory.Functor.final_iff_isIso_colimit_pre, colimit_obj_ext_iff, CompleteLattice.finite_colimit_eq_finset_univ_sup, Sigma.ι_isoColimit_hom_assoc, π_comp_colimitOpIsoOpLimit_inv_assoc, colimitIsoSwapCompColim_inv_app, colimit.hom_ext_iff, isIndObject_colimit, CategoryTheory.Functor.lanCompColimIso_inv_app, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom, map_π_preserves_coequalizer_inv_colimMap_assoc, CategoryTheory.preservesColimitNatIso_hom_app, colimitHomIsoLimitYoneda_hom_comp_π_assoc, CategoryTheory.MorphismProperty.colimitsOfShape_colimMap, colimit.w_apply, smoothSheafCommRing.ι_forgetStalk_inv_apply, ClosedUnderColimitsOfShape.colimit, colimCompFlipIsoWhiskerColim_hom_app_app, CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom, fiberwiseColimitLimitIso_inv_app, isIso_ι_initial, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom_assoc, colimit.map_post, colimitFlipIsoCompColim_hom_app, colimit.isoColimitCocone_ι_inv_assoc, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv_assoc, Cocone.isColimit_iff_isIso_colimMap_ι, π_comp_colimitOpIsoOpLimit_inv, colimitHomIsoLimitYoneda'_inv_comp_π_assoc, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, CategoryTheory.preservesColimitIso_inv_comp_desc_assoc, limitRightOpIsoOpColimit_hom_comp_ι_assoc, CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv_assoc, CategoryTheory.SmallObject.SuccStruct.arrowι_def, ι_colimitLimitIso_limit_π_assoc, colimIsoFlipCompWhiskerColim_hom_app_app, smoothSheafCommRing.ι_forgetStalk_inv_assoc, colimitPointwiseProductToProductColimit_app, colim_obj, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, colimit.ι_post_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_I₀, colimitObjIsoColimitCompEvaluation_ι_app_hom, colimit.pre_desc_assoc, colimit.pre_desc, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty, limitOpIsoOpColimit_inv_comp_π_assoc, PresheafOfModules.colimitPresheafOfModules_map, colimit.ι_desc_apply, ι_comp_colimitRightOpIsoUnopLimit_hom, ModuleCat.HasColimit.coconePointSMul_apply, AlgebraicGeometry.PresheafedSpace.colimit_presheaf, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, Sigma.ι_isoColimit_hom, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_X, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π, colimit.desc_cocone, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj, colimit.ι_desc, ι_colimitOfIsReflexivePairIsoCoequalizer_hom, fiberwiseColimCompEvaluationIso_hom_app, CategoryTheory.ι_preservesColimitIso_hom, colimit.post_post, colimit.pre_map', colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc, Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit, HasColimit.isoOfNatIso_ι_hom_assoc, CategoryTheory.FunctorToTypes.colimit.map_ι_apply, AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι, CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom, colimIsoFlipCompWhiskerColim_inv_app_app, MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app, CategoryTheory.Functor.Final.ι_colimitIso_inv_assoc, HasColimit.isoOfNatIso_hom_desc_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion_aux, CategoryTheory.instIsIsoPost_1, HomologicalComplex.coconeOfHasColimitEval_ι_app_f, colimit.pre_map, ι_comp_colimitOpIsoOpLimit_hom, limitLeftOpIsoUnopColimit_inv_comp_π, Concrete.colimit_rep_eq_of_exists, coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc, CategoryTheory.FunctorToTypes.jointly_surjective', CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit, colimitConstInitial_inv, colimit.existsUnique, ι_colimitFiberwiseColimitIso_hom, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective, colimitIsoFlipCompColim_hom_app, colimit.ι_coconeMorphism, smoothSheafCommRing.ι_forgetStalk_hom_apply, colimit.ι_map_assoc, fiberwiseColimCompColimIso_hom_app, limitUnopIsoUnopColimit_hom_comp_ι_assoc, colimit_ι_zero_cokernel_desc, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, colimitQuotientCoproduct_epi, smoothSheafCommRing.ι_forgetStalk_hom_assoc, CategoryTheory.Functor.Final.colimit_pre_isIso, colimit.comp_coconePointUniqueUpToIso_hom, π_comp_colimitRightOpIsoUnopLimit_inv, ι_comp_colimitUnopIsoOpLimit_hom_assoc, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, colimit.ι_desc_assoc, CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom_assoc, colimit.ι_desc_app_assoc, π_colimitOfIsReflexivePairIsoCoequalizer_inv, colimit.eqToHom_comp_ι, coconePointwiseProduct_pt, ι_colimitFiberwiseColimitIso_inv, coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, colimit.map_desc_assoc, ModuleCat.HasColimit.colimitCocone_pt_carrier, π_reflexiveCoequalizerIsoCoequalizer_inv, ι_reflexiveCoequalizerIsoCoequalizer_hom, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc, colimit.isoColimitCocone_ι_hom_assoc, fiberwiseColimCompColimIso_inv_app, PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom_assoc, HasColimit.isoOfNatIso_ι_hom, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_obj, colimit.cocone_x, limitOpIsoOpColimit_inv_comp_π, smoothSheaf.ι_evalHom, fiberwiseColimCompEvaluationIso_inv_app, smoothSheafCommRing.ι_evalHom_assoc, CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal, CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_pt, colimitCoyonedaHomIsoLimit_π_apply, smoothSheafCommRing.ι_forgetStalk_hom, ι_colimitPointwiseProductToProductColimit_π_assoc, colimitYonedaHomIsoLimitOp_π_apply, colimit.post_desc, colimit_map_colimitObjIsoColimitCompEvaluation_hom, coconeOfCoconeFiberwiseColimit_ι_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, colimit_map_colimitObjIsoColimitCompEvaluation_hom_assoc, colimit.w_assoc, CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom, MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, colimitIsoColimitCurryCompColim_ι_ι_inv, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc, ι_colimitConstInitial_hom, π_comp_colimitRightOpIsoUnopLimit_inv_assoc, CommRingCat.FilteredColimits.instNontrivialCarrierColimitOfIsFilteredOrEmptyOfObj, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, Concrete.colimit_exists_rep, colimit.w, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom, limitRightOpIsoOpColimit_inv_comp_π_assoc, CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom_assoc, limitLeftOpIsoUnopColimit_hom_comp_ι_assoc, CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv, AlgebraicGeometry.PresheafedSpace.colimit_carrier, π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc, colimMap_epi, TopCat.colimit_isOpen_iff, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, CategoryTheory.MorphismProperty.colimMap, colimitObjIsoColimitCompEvaluation_ι_inv, π_comp_colimitUnopIsoOpLimit_inv_assoc, PresheafOfModules.colimitPresheafOfModules_obj, IndizationClosedUnderFilteredColimitsAux.isFiltered, CategoryTheory.instSmallHomFunctorOppositeTypeColimitCompYoneda, ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc, HasBiproductsOfShape.colimIsoLim_hom_app, whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv, CategoryTheory.Functor.Final.ι_colimitIso_hom, IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_colimit, Sigma.ι_isoColimit_inv_assoc, limitLeftOpIsoUnopColimit_inv_comp_π_assoc, ι_colimitLimitToLimitColimit_π_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, CategoryTheory.ι_preservesColimitIso_inv, ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc, CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc, ι_comp_colimitLeftOpIsoUnopLimit_hom, colimitHomIsoLimitYoneda_inv_comp_π, CategoryTheory.yonedaYonedaColimit_app_inv, limitLeftOpIsoUnopColimit_hom_comp_ι, colimCompFlipIsoWhiskerColim_inv_app_app, colimit.toCostructuredArrow_map, PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom, whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv_assoc, colimit.toCostructuredArrow_obj, CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux, colimitYonedaHomIsoLimitRightOp_π_apply, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom_assoc, colimit.toOver_pt, colimit.isoColimitCocone_ι_hom, colimitLimitToLimitColimit_injective, colimit.comp_coconePointUniqueUpToIso_inv, Types.isIso_colimitPointwiseProductToProductColimit, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, colimitCoyonedaHomIsoLimitLeftOp_π_apply, colimitHomIsoLimitYoneda_inv_comp_π_assoc, limitUnopIsoUnopColimit_inv_comp_π, HasColimit.isoOfNatIso_inv_desc, Types.colimitEquivColimitType_symm_apply, colimit.ι_inv_pre_assoc, HasBiproductsOfShape.colimIsoLim_inv_app, HasColimit.isoOfNatIso_ι_inv_assoc, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, map_π_preserves_coequalizer_inv_colimMap_desc_assoc, AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f, ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc, colimit.pre_eq, colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc, colimit.ι_desc_app, limitOpIsoOpColimit_hom_comp_ι, coequalizer.π_colimMap_desc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, CategoryTheory.MonoidalCategory.DayFunctor.ι_comp_isoPointwiseLeftKanExtension_inv, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase, CategoryTheory.Functor.lanCompColimIso_hom_app, isIso_ι_of_isTerminal, ι_colimitConstInitial_hom_assoc, Types.colimitEquivColimitType_apply, colimitFlipCompColimIsoColimitCompColim_ι_ι_inv, limitRightOpIsoOpColimit_inv_comp_π, instEpiDescι, CategoryTheory.colimitYonedaHomEquiv_π_apply, π_tensor_id_preserves_coequalizer_inv_colimMap_desc, colimitFlipIsoCompColim_inv_app, colimitLimitToLimitColimit_surjective, CategoryTheory.Functor.Final.colimitIso_inv, ι_comp_colimitUnopIsoOpLimit_hom, colimitHomIsoLimitYoneda'_inv_comp_π, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom
|
coneOfAdj 📖 | CompOp | 3 mathmath: coneOfAdj_pt, isLimitConeOfAdj_lift, coneOfAdj_π
|
constLimAdj 📖 | CompOp | 1 mathmath: CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app
|
getColimitCocone 📖 | CompOp | — |
getLimitCone 📖 | CompOp | — |
isColimitEquivIsLimitOp 📖 | CompOp | — |
isColimitOfOp 📖 | CompOp | — |
isColimitOfUnop 📖 | CompOp | — |
isLimitConeOfAdj 📖 | CompOp | 1 mathmath: isLimitConeOfAdj_lift
|
isLimitEquivIsColimitOp 📖 | CompOp | — |
isLimitOfOp 📖 | CompOp | — |
isLimitOfUnop 📖 | CompOp | — |
lim 📖 | CompOp | 66 mathmath: colimitLimitToLimitColimit_isIso, yonedaCompLimIsoCocones_inv_app, coyonedaCompLimIsoCones_inv_app, limitIsoLimitCurryCompLim_hom_π_π_assoc, CategoryTheory.HasExactLimitsOfShape.preservesFiniteColimits, lim_map, CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app, CategoryTheory.Functor.ranCompLimIso_inv_app, instIsRightAdjointFunctorLim, ι_colimitLimitToLimitColimit_π, limitFlipCompLimIsoLimitCompLim_hom_π_π, limitIsoSwapCompLim_hom_app, limitIsoFlipCompLim_hom_app, opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_app, limCompFlipIsoWhiskerLim_inv_app_app, CategoryTheory.Mon.limit_mon_mul, limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π, yonedaCompLimIsoCocones_hom_app_app, colimitLimitToLimitColimitCone_hom, DiagramOfCones.mkOfHasLimits_map_hom, limitFlipCompLimIsoLimitCompLim_inv_π_π, lim_ε_π_assoc, LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim, whiskeringLimYonedaIsoCones_inv_app_app, CategoryTheory.preservesLimitNatIso_inv_app, lim_obj, lim_ε_π, limitUncurryIsoLimitCompLim_inv_π, limitFlipIsoCompLim_inv_app, limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc, limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π, lim_μ_π_assoc, limIsoFlipCompWhiskerLim_hom_app_app, limitUncurryIsoLimitCompLim_hom_π_π_assoc, limitIsoSwapCompLim_inv_app, limit.map_pre', limitIsoLimitCurryCompLim_inv_π, CategoryTheory.Localization.HasProductsOfShapeAux.inverts, whiskeringLimYonedaIsoCones_hom_app_app_app, limMap_eq, ι_colimitLimitToLimitColimit_π_apply, limitIsoLimitCurryCompLim_inv_π_assoc, limCompFlipIsoWhiskerLim_hom_app_app, limitIsoLimitCurryCompLim_hom_π_π, CategoryTheory.Mon.limit_mon_one, limitFlipIsoCompLim_hom_app, limitUncurryIsoLimitCompLim_hom_π_π, limIsoFlipCompWhiskerLim_inv_app_app, limit.id_pre, limitIsoFlipCompLim_inv_app, limit.map_pre, HasBiproductsOfShape.colimIsoLim_hom_app, DiagramOfCones.mkOfHasLimits_conePoints, CategoryTheory.preservesLimitNatIso_hom_app, ι_colimitLimitToLimitColimit_π_assoc, CategoryTheory.Adjunction.lim_preservesLimits, CategoryTheory.Functor.ranCompLimIso_hom_app, coyonedaCompLimIsoCones_hom_app_app, colimitLimitToLimitColimit_injective, lim_μ_π, limitUncurryIsoLimitCompLim_inv_π_assoc, opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app, HasBiproductsOfShape.colimIsoLim_inv_app, limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc, colimitLimitToLimitColimit_surjective, CategoryTheory.instPreservesColimitsOfShapeFunctorLim
|
limMap 📖 | CompOp | 26 mathmath: limMap_π, HomologicalComplex.coneOfHasLimitEval_pt_d, PresheafOfModules.limitPresheafOfModules_map, lim_map, limitIsoSwapCompLim_hom_app, CategoryTheory.Mon.limit_mon_mul, Types.Limit.map_π_apply', limMap_π_assoc, limMap_mono, CategoryTheory.MorphismProperty.limMap, limit.map_post, IsLimit.isIso_limMap_π, limitObjIsoLimitCompEvaluation_inv_limit_map, limit_map_limitObjIsoLimitCompEvaluation_hom_assoc, limMap_mono', limitIsoSwapCompLim_inv_app, Cone.isLimit_iff_isIso_limMap_π, Types.Limit.map_π_apply, limit.lift_map, limMap_eq, HomologicalComplex.coneOfHasLimitEval_π_app_f, CategoryTheory.Mon.limit_mon_one, limit.lift_map_assoc, limitObjIsoLimitCompEvaluation_inv_limit_map_assoc, CategoryTheory.MorphismProperty.limitsOfShape_limMap, limit_map_limitObjIsoLimitCompEvaluation_hom
|
limYoneda 📖 | CompOp | — |
limit 📖 | CompOp | 295 mathmath: limMap_π, colimitHomIsoLimitYoneda'_hom_comp_π, IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac, colimitHomIsoLimitYoneda_hom_comp_π, isIndObject_limit_of_discrete, limitUnopIsoUnopColimit_hom_comp_ι, limit.toStructuredArrow_obj, MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, colimitLimitToLimitColimit_isIso, isIso_π_of_isTerminal, limitSubobjectProduct_mono, ι_comp_colimitOpIsoOpLimit_hom_assoc, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc, HasLimit.isoOfNatIso_inv_π_assoc, HasLimit.lift_isoOfNatIso_hom, CategoryTheory.Functor.Initial.limitIso_hom, yonedaCompLimIsoCocones_inv_app, PresheafOfModules.limitPresheafOfModules_map, colimitCoyonedaHomIsoLimit'_π_apply, coyonedaCompLimIsoCones_inv_app, limitConstTerminal_inv_π_assoc, limitOpIsoOpColimit_hom_comp_ι_assoc, CategoryTheory.IsFiltered.iff_nonempty_limit, limit.w_assoc, limitIsoLimitCurryCompLim_hom_π_π_assoc, limitObjIsoLimitCompEvaluation_inv_π_app, CategoryTheory.Functor.ranCompLimIso_inv_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion, limit.toStructuredArrow_map, colimitYonedaHomIsoLimit'_π_apply, π_comp_colimitLeftOpIsoUnopLimit_inv, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π_assoc, colimitHomIsoLimitYoneda'_hom_comp_π_assoc, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, CategoryTheory.Functor.Initial.limitIso_inv, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π_assoc, isIso_π_terminal, CategoryTheory.IsCofiltered.iff_nonempty_limit, fiberwiseColimitLimitIso_hom_app, limit.lift_post, ι_colimitLimitIso_limit_π, ι_colimitLimitToLimitColimit_π, π_comp_colimitUnopIsoOpLimit_inv, limit.pre_post, limitConstTerminal_hom, limitFlipCompLimIsoLimitCompLim_hom_π_π, instMonoLiftπ, limitIsoSwapCompLim_hom_app, coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc, limitIsoFlipCompLim_hom_app, limitCompCoyonedaIsoCone_hom_app, ι_comp_colimitRightOpIsoUnopLimit_hom_assoc, limit.post_π, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_π_app_coe, CategoryTheory.Cat.HasLimits.limitCone_π_app, PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom, coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π, limit.isoLimitCone_hom_π_assoc, AlgebraicGeometry.IsOpenImmersion.instπWalkingCospanSchemeCospanOne, limit.pre_π_assoc, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc, limCompFlipIsoWhiskerLim_inv_app_app, CategoryTheory.Cat.HasLimits.limitConeX_α, CategoryTheory.Mon.limit_mon_mul, colimitYonedaHomIsoLimit_π_apply, limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π, CategoryTheory.preservesLimitIso_inv_π_assoc, MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, Pi.isoLimit_inv_π, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion, colimitLimitToLimitColimitCone_hom, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, limit.isoLimitCone_hom_π, π_comp_colimitLeftOpIsoUnopLimit_inv_assoc, limMap_π_assoc, limitFlipCompLimIsoLimitCompLim_inv_π_π, CategoryTheory.lift_comp_preservesLimitIso_hom_assoc, limitUnopIsoUnopColimit_inv_comp_π_assoc, CategoryTheory.preservesLimitIso_inv_π, whiskeringLimYonedaIsoCones_inv_app_app, limit.π_comp_eqToHom_assoc, colimitCoyonedaHomIsoLimitUnop_π_apply, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, limitRightOpIsoOpColimit_hom_comp_ι, limit.π_comp_eqToHom, HasLimit.isoOfEquivalence_hom_π, limitConstTerminal_inv_π, CategoryTheory.preservesLimitNatIso_inv_app, CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom, π_comp_colimitOpIsoOpLimit_inv_assoc, SingleObj.Types.limitEquivFixedPoints_symm_apply, limMap_mono, CategoryTheory.ObjectProperty.prop_limit, CategoryTheory.lift_comp_preservesLimitIso_hom, TopCat.isOpenEmbedding_of_pullback, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, isIndObject_limit_of_discrete_of_hasLimitsOfShape, HasLimit.isoOfNatIso_inv_π, limit.cone_x, CategoryTheory.Cat.HasLimits.limitConeX_str, colimitHomIsoLimitYoneda_hom_comp_π_assoc, limit.existsUnique, Types.limitEquivSections_symm_apply, CategoryTheory.MorphismProperty.limMap, limitObjIsoLimitCompEvaluation_hom_π, limit.post_π_assoc, CategoryTheory.Functor.ranObjObjIsoLimit_inv_π_assoc, CategoryTheory.Cat.HasLimits.id_def, limitCompWhiskeringLeftIsoCompLimit_inv_π_assoc, fiberwiseColimitLimitIso_inv_app, PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app, CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π_assoc, lim_obj, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi, isIndObject_limit_comp_yoneda, limit.post_post, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc, limit.lift_π_app, limit_obj_ext_iff, TopCat.limit_isSheaf, π_comp_colimitOpIsoOpLimit_inv, colimitHomIsoLimitYoneda'_inv_comp_π_assoc, limitRightOpIsoOpColimit_hom_comp_ι_assoc, CompleteLattice.finite_limit_eq_finset_univ_inf, CategoryTheory.Functor.ranObjObjIsoLimit_hom_π_assoc, ι_colimitLimitIso_limit_π_assoc, limitUncurryIsoLimitCompLim_inv_π, AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso, limit.map_post, limit.isoLimitCone_inv_π_assoc, limitFlipIsoCompLim_inv_app, HasLimit.isoOfNatIso_hom_π_assoc, MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app, limitOpIsoOpColimit_inv_comp_π_assoc, limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc, ι_comp_colimitRightOpIsoUnopLimit_hom, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π, AlgebraicGeometry.PresheafedSpace.colimit_presheaf, IsLimit.isIso_limMap_π, limit.lift_π_apply, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π, limitObjIsoLimitCompEvaluation_inv_limit_map, limit_map_limitObjIsoLimitCompEvaluation_hom_assoc, limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π, ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt, limMap_mono', AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, limitCompYonedaIsoCocone_inv, MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π, CommRingCat.equalizer_ι_isLocalHom', CategoryTheory.preservesLimitIso_hom_π_assoc, lim_μ_π_assoc, limit.lift_pre, limIsoFlipCompWhiskerLim_hom_app_app, CategoryTheory.Functor.pointwiseRightKanExtension_obj, MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, limitCompCoyonedaIsoCone_inv, CategoryTheory.Functor.rightAdjointObjIsDefined_limit, limitUncurryIsoLimitCompLim_hom_π_π_assoc, limitIsoSwapCompLim_inv_app, SingleObj.Types.limitEquivFixedPoints_apply_coe, ι_comp_colimitOpIsoOpLimit_hom, limitLeftOpIsoUnopColimit_inv_comp_π, coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc, PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π_assoc, limit.homIso_hom, limit.map_pre', limitUnopIsoUnopColimit_hom_comp_ι_assoc, π_comp_colimitRightOpIsoUnopLimit_inv, ι_comp_colimitUnopIsoOpLimit_hom_assoc, PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π_assoc, Cone.isLimit_iff_isIso_limMap_π, limitIsoLimitCurryCompLim_inv_π, CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π_assoc, limit.hom_ext_iff, limit.lift_π_assoc, CategoryTheory.Functor.ranObjObjIsoLimit_hom_π, CategoryTheory.Mon.limit_X, CommRingCat.equalizer_ι_isLocalHom, coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, limit.pre_eq, limit.lift_map, CategoryTheory.Functor.pointwiseRightKanExtension_map, limitObjIsoLimitCompEvaluation_inv_π_app_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion, PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π_assoc, ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc, CategoryTheory.Cat.HasLimits.comp_def, HomologicalComplex.coneOfHasLimitEval_pt_X, ClosedUnderLimitsOfShape.limit, limit.isoLimitCone_inv_π, limitOpIsoOpColimit_inv_comp_π, HomologicalComplex.coneOfHasLimitEval_π_app_f, isIso_π_of_isInitial, Types.limitEquivSections_apply, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π, CategoryTheory.preservesLimitIso_hom_π, limitIsoLimitCurryCompLim_inv_π_assoc, limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π_assoc, colimitCoyonedaHomIsoLimit_π_apply, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc, limitObjIsoLimitCompEvaluation_hom_π_assoc, limCompFlipIsoWhiskerLim_hom_app_app, limitIsoLimitCurryCompLim_hom_π_π, limitCompYonedaIsoCocone_hom_app, colimitYonedaHomIsoLimitOp_π_apply, limitCompWhiskeringLeftIsoCompLimit_inv_π, CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor, CategoryTheory.Mon.limit_mon_one, CategoryTheory.Functor.ranObjObjIsoLimit_inv_π, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, Pi.isoLimit_hom_π, limit_π_isIso_of_is_strict_terminal, π_comp_colimitRightOpIsoUnopLimit_inv_assoc, CompleteLattice.limit_eq_iInf, limitFlipIsoCompLim_hom_app, limitUncurryIsoLimitCompLim_hom_π_π, limIsoFlipCompWhiskerLim_inv_app_app, limit.lift_π_app_assoc, limitRightOpIsoOpColimit_inv_comp_π_assoc, limitIsoFlipCompLim_inv_app, limitLeftOpIsoUnopColimit_hom_comp_ι_assoc, limit.map_pre, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac, π_comp_colimitUnopIsoOpLimit_inv_assoc, Pi.isoLimit_hom_π_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π, PresheafOfModules.limitPresheafOfModules_obj, isIso_π_initial, ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc, HasLimit.isoOfNatIso_hom_π, HasBiproductsOfShape.colimIsoLim_hom_app, CategoryTheory.preservesLimitNatIso_hom_app, IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_colimit, CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π, limitLeftOpIsoUnopColimit_inv_comp_π_assoc, ι_colimitLimitToLimitColimit_π_assoc, CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone, ι_comp_colimitLeftOpIsoUnopLimit_hom, Pi.isoLimit_inv_π_assoc, colimitHomIsoLimitYoneda_inv_comp_π, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π, PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post, limitLeftOpIsoUnopColimit_hom_comp_ι, HasLimit.isoOfEquivalence_inv_π, CategoryTheory.Functor.Initial.limit_pre_isIso, CategoryTheory.Functor.ranCompLimIso_hom_app, limit.pre_pre, TopCat.limit_topology, HasLimit.lift_isoOfNatIso_inv, limit.lift_map_assoc, CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π, CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement, limit.lift_π, colimitYonedaHomIsoLimitRightOp_π_apply, limitObjIsoLimitCompEvaluation_inv_limit_map_assoc, limit.lift_cone, colimitLimitToLimitColimit_injective, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π_assoc, lim_μ_π, colimitCoyonedaHomIsoLimitLeftOp_π_apply, limitUncurryIsoLimitCompLim_inv_π_assoc, HasLimit.lift_isoOfNatIso_hom_assoc, colimitHomIsoLimitYoneda_inv_comp_π_assoc, limitUnopIsoUnopColimit_inv_comp_π, opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app, HasBiproductsOfShape.colimIsoLim_inv_app, CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi, limit.w_apply, limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_fst, limit.lift_extend, CategoryTheory.instIsIsoPost, limitOpIsoOpColimit_hom_comp_ι, CategoryTheory.MorphismProperty.limitsOfShape_limMap, limit.w, limit.pre_π, limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π, HasLimit.lift_isoOfNatIso_inv_assoc, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π, limitRightOpIsoOpColimit_inv_comp_π, limit_map_limitObjIsoLimitCompEvaluation_hom, CategoryTheory.colimitYonedaHomEquiv_π_apply, colimitLimitToLimitColimit_surjective, TopCat.isEmbedding_of_pullback, ι_comp_colimitUnopIsoOpLimit_hom, colimitHomIsoLimitYoneda'_inv_comp_π
|