IsLimit

📁 Source: Mathlib/CategoryTheory/Limits/IsLimit.lean

Statistics

Metric	Count
Definitions IsColimit, coconeOfHom, colimitCocone, homOfCocone, coconePointUniqueUpToIso, coconePointsIsoOfEquivalence, coconePointsIsoOfNatIso, corepresentableBy, desc, descCoconeMorphism, equivIsoColimit, equivOfNatIsoOfIso, extendIso, extendIsoEquiv, homEquiv, homIso, homIso', isoUniqueCoconeMorphism, map, mapCoconeEquiv, mkCoconeMorphism, natIso, ofCoconeEquiv, ofCorepresentableBy, ofExistsUnique, ofExtendIso, ofFaithful, ofIsoColimit, ofLeftAdjoint, ofPointIso, ofWhiskerEquivalence, precomposeHomEquiv, precomposeInvEquiv, uniqueUpToIso, whiskerEquivalence, whiskerEquivalenceEquiv, IsLimit, coneOfHom, homOfCone, limitCone, conePointUniqueUpToIso, conePointsIsoOfEquivalence, conePointsIsoOfNatIso, equivIsoLimit, equivOfNatIsoOfIso, extendIso, extendIsoEquiv, homEquiv, homIso, homIso', isoUniqueConeMorphism, liftConeMorphism, map, mapConeEquiv, mkConeMorphism, natIso, ofConeEquiv, ofExistsUnique, ofExtendIso, ofFaithful, ofIsoLimit, ofPointIso, ofRepresentableBy, ofRightAdjoint, ofWhiskerEquivalence, postcomposeHomEquiv, postcomposeInvEquiv, representableBy, uniqueUpToIso, whiskerEquivalence, whiskerEquivalenceEquiv	71
Theorems coconeOfHom_fac, coconeOfHom_homOfCocone, cocone_fac, homOfCocone_coconeOfHom, coconePointUniqueUpToIso_hom_desc, coconePointUniqueUpToIso_hom_desc_assoc, coconePointUniqueUpToIso_inv_desc, coconePointUniqueUpToIso_inv_desc_assoc, coconePointsIsoOfEquivalence_hom, coconePointsIsoOfEquivalence_inv, coconePointsIsoOfNatIso_hom, coconePointsIsoOfNatIso_hom_desc, coconePointsIsoOfNatIso_hom_desc_assoc, coconePointsIsoOfNatIso_inv, coconePointsIsoOfNatIso_inv_desc, coconePointsIsoOfNatIso_inv_desc_assoc, comp_coconePointUniqueUpToIso_hom, comp_coconePointUniqueUpToIso_hom_assoc, comp_coconePointUniqueUpToIso_inv, comp_coconePointUniqueUpToIso_inv_assoc, comp_coconePointsIsoOfNatIso_hom, comp_coconePointsIsoOfNatIso_hom_assoc, comp_coconePointsIsoOfNatIso_inv, comp_coconePointsIsoOfNatIso_inv_assoc, descCoconeMorphism_hom, desc_self, equivIsoColimit_apply, equivIsoColimit_symm_apply, existsUnique, fac, fac_assoc, homEquiv_apply, homEquiv_symm_naturality, homIso_hom, hom_desc, hom_ext, hom_isIso, mkCoconeMorphism_desc, nonempty_isColimit_iff_isIso_desc, ofCoconeEquiv_apply_desc, ofCoconeEquiv_symm_apply_desc, ofIsoColimit_desc, subsingleton, uniq, uniq_cocone_morphism, uniqueUpToIso_hom, uniqueUpToIso_inv, ι_app_homEquiv_symm, ι_app_homEquiv_symm_assoc, ι_map, ι_map_assoc, coneOfHom_fac, coneOfHom_homOfCone, cone_fac, homOfCone_coneOfHom, conePointUniqueUpToIso_hom_comp, conePointUniqueUpToIso_hom_comp_assoc, conePointUniqueUpToIso_inv_comp, conePointUniqueUpToIso_inv_comp_assoc, conePointsIsoOfEquivalence_hom, conePointsIsoOfEquivalence_inv, conePointsIsoOfNatIso_hom, conePointsIsoOfNatIso_hom_comp, conePointsIsoOfNatIso_hom_comp_assoc, conePointsIsoOfNatIso_inv, conePointsIsoOfNatIso_inv_comp, conePointsIsoOfNatIso_inv_comp_assoc, equivIsoLimit_apply, equivIsoLimit_symm_apply, existsUnique, fac, fac_assoc, homEquiv_apply, homEquiv_symm_naturality, homEquiv_symm_π_app, homEquiv_symm_π_app_assoc, homIso_hom, hom_ext, hom_isIso, hom_lift, liftConeMorphism_hom, lift_comp_conePointUniqueUpToIso_hom, lift_comp_conePointUniqueUpToIso_hom_assoc, lift_comp_conePointUniqueUpToIso_inv, lift_comp_conePointUniqueUpToIso_inv_assoc, lift_comp_conePointsIsoOfNatIso_hom, lift_comp_conePointsIsoOfNatIso_hom_assoc, lift_comp_conePointsIsoOfNatIso_inv, lift_comp_conePointsIsoOfNatIso_inv_assoc, lift_self, map_π, map_π_assoc, mkConeMorphism_lift, nonempty_isLimit_iff_isIso_lift, ofConeEquiv_apply_desc, ofConeEquiv_symm_apply_desc, ofIsoLimit_lift, subsingleton, uniq, uniq_cone_morphism, uniqueUpToIso_hom, uniqueUpToIso_inv	102
Total	173

CategoryTheory.Limits

Definitions

Name	Category	Theorems
IsColimit 📖	CompData	52 math math: TopCat.binaryCofan_isColimit_iff, Types.binaryCofan_isColimit_iff, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, Types.isColimit_iff_coconeTypesIsColimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left, CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan, CategoryTheory.Functor.Final.colimitCoconeOfComp_isColimit, AddCommGrpCat.isColimit_iff_bijective_desc, IsColimit.equivIsoColimit_apply, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, Cofan.isColimit_iff_isIso_sigmaDesc, CategoryTheory.BinaryCofan.isVanKampen_iff, CategoryTheory.IsPushout.isColimit', IsColimit.nonempty_isColimit_iff_isIso_desc, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback, CategoryTheory.is_coprod_iff_isPushout, CategoryTheory.Functor.Final.colimitCoconeComp_isColimit, IsColimit.ofCoconeEquiv_symm_apply_desc, IsInitial.to_eq_descCoconeMorphism, CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand, Types.isConnected_iff_isColimit_pUnitCocone, CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit, BinaryCofan.isColimit_iff_isIso_inl, PreservesColimit.preserves, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel, BinaryCofan.isColimit_iff_isIso_inr, AlgebraicGeometry.nonempty_isColimit_cofanMk_of, CategoryTheory.BicartesianSq.isColimit', IsColimit.descCoconeMorphism_eq_isInitial_to, Cocone.isColimit_iff_isIso_colimMap_ι, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, CategoryTheory.Functor.isDenseAt_iff, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, SheafOfModules.Presentation.map_relations_I, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, IsColimit.ofCoconeEquiv_apply_desc, CategoryTheory.Square.isPushout_iff, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit, IsColimit.equivIsoColimit_symm_apply, ReflectsColimit.reflects, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right, TopCat.nonempty_isColimit_iff_eq_coinduced, AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl, IsColimit.subsingleton, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right, Cofan.nonempty_isColimit_iff_isIso_sigmaDesc, CategoryTheory.Presieve.Extensive.arrows_nonempty_isColimit, CategoryTheory.Functor.CoconeTypes.isColimit_iff, Cofan.isColimit_cofanTypes_iff, Cofan.nonempty_isColimit_iff_bijective_fromSigma, AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone, PreservesColimit₂.nonempty_isColimit_mapCocone₂
IsLimit 📖	CompData	44 math math: IsLimit.ofConeEquiv_symm_apply_desc, IsLimit.equivIsoLimit_apply, CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition, IsLimit.liftConeMorphism_eq_isTerminal_from, PreservesLimit.preserves, CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff, CategoryTheory.IsPullback.isLimit', IsLimit.nonempty_isLimit_iff_isIso_lift, IsLimit.subsingleton, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, ReflectsLimit.reflects, CategoryTheory.Functor.Initial.limitConeComp_isLimit, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, TopCat.nonempty_isLimit_iff_eq_induced, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, IsLimit.equivIsoLimit_symm_apply, IsLimit.ofConeEquiv_apply_desc, CategoryTheory.Equalizer.Presieve.sheaf_condition, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.Square.isPullback_iff, CategoryTheory.Presheaf.isSheaf_iff_isLimit, CategoryTheory.Presheaf.isSheaf_iff_multifork, PreservesLimit₂.nonempty_isLimit_mapCone₂, CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, BinaryFan.isLimit_iff_isIso_fst, CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel, Cone.isLimit_iff_isIso_limMap_π, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, Fan.nonempty_isLimit_iff_isIso_piLift, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, BinaryFan.isLimit_iff_isIso_snd, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, IsTerminal.from_eq_liftConeMorphism, Types.isLimit_iff_bijective_sectionOfCone, Multifork.isLimit_types_iff, Types.isLimit_iff, Types.type_equalizer_iff_unique, CategoryTheory.Functor.Initial.limitConeOfComp_isLimit, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology

CategoryTheory.Limits.IsColimit

Definitions

Name	Category	Theorems
coconePointUniqueUpToIso 📖	CompOp	13 math math: CategoryTheory.Limits.opCoproductIsoProduct'_comp_self, comp_coconePointUniqueUpToIso_inv, coconePointUniqueUpToIso_inv_desc_assoc, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv_assoc, comp_coconePointUniqueUpToIso_inv_assoc, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc, coconePointUniqueUpToIso_inv_desc, coconePointUniqueUpToIso_hom_desc_assoc, comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom, comp_coconePointUniqueUpToIso_hom_assoc, coconePointUniqueUpToIso_hom_desc, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv
coconePointsIsoOfEquivalence 📖	CompOp	2 math math: coconePointsIsoOfEquivalence_hom, coconePointsIsoOfEquivalence_inv
coconePointsIsoOfNatIso 📖	CompOp	10 math math: comp_coconePointsIsoOfNatIso_hom_assoc, coconePointsIsoOfNatIso_hom_desc_assoc, coconePointsIsoOfNatIso_hom, comp_coconePointsIsoOfNatIso_hom, coconePointsIsoOfNatIso_inv_desc_assoc, coconePointsIsoOfNatIso_hom_desc, coconePointsIsoOfNatIso_inv_desc, comp_coconePointsIsoOfNatIso_inv_assoc, comp_coconePointsIsoOfNatIso_inv, coconePointsIsoOfNatIso_inv
corepresentableBy 📖	CompOp	—
desc 📖	CompOp	110 math math: CategoryTheory.Limits.Bicone.π_of_isColimit, CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_φ, CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift, fac, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension_desc, CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc, CategoryTheory.Monad.beckCoequalizer_desc, CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom, CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc, CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift, CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift, CategoryTheory.Limits.Types.binaryCoproductColimit_desc, CategoryTheory.Limits.mkCofanColimit_desc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, nonempty_isColimit_iff_isIso_desc, mkCoconeMorphism_desc, CategoryTheory.Limits.Multicofork.IsColimit.mk_desc, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, CategoryTheory.Limits.Cofan.IsColimit.inj_desc, CategoryTheory.ShortComplex.RightHomologyData.wι_assoc, desc_self, ofCoconeEquiv_symm_apply_desc, coconePointsIsoOfNatIso_hom_desc_assoc, CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_f, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, coconePointUniqueUpToIso_inv_desc_assoc, CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc, CategoryTheory.Limits.cokernelBiprodInlIso_inv, CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift, CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc, ModuleCat.directLimitIsColimit_desc, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.snd_of_isColimit, CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc, CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc, CategoryTheory.Limits.cokernelBiprodInrIso_inv, Condensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc, coconePointsIsoOfEquivalence_hom, CategoryTheory.Limits.isLimitConeUnopOfCocone_lift, CategoryTheory.Limits.IndObjectPresentation.yoneda_isColimit_desc, CategoryTheory.Comma.coconeOfPreserves_ι_app_right, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff, CategoryTheory.Comma.coconeOfPreserves_pt_hom, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc_app, CategoryTheory.Limits.cokernelBiproductιIso_inv, coconePointsIsoOfNatIso_inv_desc_assoc, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_fst, coconePointsIsoOfEquivalence_inv, CategoryTheory.ShortComplex.RightHomologyData.wι, coconePointsIsoOfNatIso_hom_desc, CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift, coconePointUniqueUpToIso_inv_desc, CategoryTheory.Comma.coconeOfPreserves_ι_app_left, CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f, CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc, coconePointUniqueUpToIso_hom_desc_assoc, CategoryTheory.FunctorToTypes.binaryCoproductColimit_desc, CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc, uniq, CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift, coconePointsIsoOfNatIso_inv_desc, ofCoconeEquiv_apply_desc, CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc, CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_, descCoconeMorphism_hom, CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_a, hom_desc, CommRingCat.coproductCoconeIsColimit_desc, CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift, CategoryTheory.Limits.fst_of_isColimit, CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift, CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app, pushoutCoconeEquivBinaryCofanFunctor_desc_right, CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc, CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.Limits.Bicone.ofColimitCocone_π, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f, CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe, CategoryTheory.Limits.combineCocones_ι_app_app, CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc, ofIsoColimit_desc, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_snd, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app, CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift, CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc, CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift, CategoryTheory.Limits.combineCocones_pt_map, CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc, coconePointUniqueUpToIso_hom_desc, CategoryTheory.preserves_desc_mapCocone, CategoryTheory.Limits.CompleteLattice.colimitCocone_isColimit_desc, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc, CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc, CategoryTheory.Limits.coconeOfCoconeCurry_ι_app, CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc, fac_assoc, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv, CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f, CategoryTheory.Limits.colimit.pre_eq, CategoryTheory.Limits.isCokernelEpiComp_desc, CategoryTheory.Limits.colimit.isColimit_desc
descCoconeMorphism 📖	CompOp	8 math math: uniqueUpToIso_hom, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, ofCoconeEquiv_symm_apply_desc, CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism, descCoconeMorphism_eq_isInitial_to, ofCoconeEquiv_apply_desc, descCoconeMorphism_hom, uniqueUpToIso_inv
equivIsoColimit 📖	CompOp	2 math math: equivIsoColimit_apply, equivIsoColimit_symm_apply
equivOfNatIsoOfIso 📖	CompOp	1 math math: SheafOfModules.Presentation.map_relations_I
extendIso 📖	CompOp	—
extendIsoEquiv 📖	CompOp	—
homEquiv 📖	CompOp	6 math math: homEquiv_apply, homEquiv_symm_naturality, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm, ι_app_homEquiv_symm_assoc, ι_app_homEquiv_symm, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc
homIso 📖	CompOp	1 math math: homIso_hom
homIso' 📖	CompOp	—
isoUniqueCoconeMorphism 📖	CompOp	—
map 📖	CompOp	12 math math: CategoryTheory.IndParallelPairPresentation.hf, CategoryTheory.NonemptyParallelPairPresentationAux.hf, ι_map, ι_map_assoc, coconePointsIsoOfNatIso_hom_desc_assoc, coconePointsIsoOfNatIso_hom, coconePointsIsoOfNatIso_inv_desc_assoc, coconePointsIsoOfNatIso_hom_desc, coconePointsIsoOfNatIso_inv_desc, CategoryTheory.IndParallelPairPresentation.hg, coconePointsIsoOfNatIso_inv, CategoryTheory.NonemptyParallelPairPresentationAux.hg
mapCoconeEquiv 📖	CompOp	—
mkCoconeMorphism 📖	CompOp	1 math math: mkCoconeMorphism_desc
natIso 📖	CompOp	—
ofCoconeEquiv 📖	CompOp	2 math math: ofCoconeEquiv_symm_apply_desc, ofCoconeEquiv_apply_desc
ofCorepresentableBy 📖	CompOp	—
ofExistsUnique 📖	CompOp	—
ofExtendIso 📖	CompOp	—
ofFaithful 📖	CompOp	—
ofIsoColimit 📖	CompOp	6 math math: equivIsoColimit_apply, CategoryTheory.TransfiniteCompositionOfShape.map_isColimit, SimplicialObject.Splitting.ofIso_isColimit', equivIsoColimit_symm_apply, CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isColimit, ofIsoColimit_desc
ofLeftAdjoint 📖	CompOp	1 math math: CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right
ofPointIso 📖	CompOp	—
ofWhiskerEquivalence 📖	CompOp	—
precomposeHomEquiv 📖	CompOp	—
precomposeInvEquiv 📖	CompOp	—
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_hom, uniqueUpToIso_inv
whiskerEquivalence 📖	CompOp	3 math math: HomotopicalAlgebra.AttachCells.reindex_isColimit₂, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isColimit, HomotopicalAlgebra.AttachCells.reindex_isColimit₁
whiskerEquivalenceEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconePointUniqueUpToIso_hom_desc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.hom coconePointUniqueUpToIso desc	—	uniq comp_coconePointUniqueUpToIso_hom_assoc fac
coconePointUniqueUpToIso_hom_desc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.hom coconePointUniqueUpToIso desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coconePointUniqueUpToIso_hom_desc
coconePointUniqueUpToIso_inv_desc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.inv coconePointUniqueUpToIso desc	—	uniq comp_coconePointUniqueUpToIso_inv_assoc fac
coconePointUniqueUpToIso_inv_desc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.inv coconePointUniqueUpToIso desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coconePointUniqueUpToIso_inv_desc
coconePointsIsoOfEquivalence_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cocone.pt coconePointsIsoOfEquivalence desc CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.Cocones.equivalenceOfReindexing	—	—
coconePointsIsoOfEquivalence_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cocone.pt coconePointsIsoOfEquivalence desc CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.Cocones.equivalenceOfReindexing CategoryTheory.Equivalence.symm CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.symm CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.Equivalence.invFunIdAssoc	—	—
coconePointsIsoOfNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cocone.pt coconePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	—
coconePointsIsoOfNatIso_hom_desc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.hom coconePointsIsoOfNatIso desc map CategoryTheory.Functor CategoryTheory.Functor.category	—	hom_ext ι_map_assoc fac ι_map
coconePointsIsoOfNatIso_hom_desc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.hom coconePointsIsoOfNatIso desc map CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coconePointsIsoOfNatIso_hom_desc
coconePointsIsoOfNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cocone.pt coconePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	—
coconePointsIsoOfNatIso_inv_desc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.inv coconePointsIsoOfNatIso desc map CategoryTheory.Functor CategoryTheory.Functor.category	—	hom_ext ι_map_assoc fac ι_map
coconePointsIsoOfNatIso_inv_desc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.inv coconePointsIsoOfNatIso desc map CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coconePointsIsoOfNatIso_inv_desc
comp_coconePointUniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.hom coconePointUniqueUpToIso	—	CategoryTheory.Limits.CoconeMorphism.w
comp_coconePointUniqueUpToIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.hom coconePointUniqueUpToIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_coconePointUniqueUpToIso_hom
comp_coconePointUniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv coconePointUniqueUpToIso	—	CategoryTheory.Limits.CoconeMorphism.w
comp_coconePointUniqueUpToIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv coconePointUniqueUpToIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_coconePointUniqueUpToIso_inv
comp_coconePointsIsoOfNatIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.hom coconePointsIsoOfNatIso	—	ι_map
comp_coconePointsIsoOfNatIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.hom coconePointsIsoOfNatIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_coconePointsIsoOfNatIso_hom
comp_coconePointsIsoOfNatIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv coconePointsIsoOfNatIso	—	ι_map
comp_coconePointsIsoOfNatIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv coconePointsIsoOfNatIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_coconePointsIsoOfNatIso_inv
descCoconeMorphism_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom descCoconeMorphism desc	—	—
desc_self 📖	mathematical	—	desc CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt	—	uniq CategoryTheory.Category.comp_id
equivIsoColimit_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Limits.IsColimit EquivLike.toFunLike Equiv.instEquivLike equivIsoColimit ofIsoColimit	—	—
equivIsoColimit_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Limits.IsColimit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivIsoColimit ofIsoColimit CategoryTheory.Iso.symm CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category	—	—
existsUnique 📖	mathematical	—	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt	—	fac uniq
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι desc	—	—
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.Cocone.extend	—	—
homEquiv_symm_naturality 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	Equiv.injective Equiv.apply_symm_apply CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.ext' ι_app_homEquiv_symm_assoc
homIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const homIso CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.Cocone.extend	—	—
hom_desc 📖	mathematical	—	desc CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	uniq CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	—	hom_desc
hom_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category	—	uniq_cocone_morphism
mkCoconeMorphism_desc 📖	mathematical	—	desc mkCoconeMorphism CategoryTheory.Limits.CoconeMorphism.hom	—	—
nonempty_isColimit_iff_isIso_desc 📖	mathematical	—	CategoryTheory.Limits.IsColimit CategoryTheory.IsIso CategoryTheory.Limits.Cocone.pt desc	—	hom_ext fac_assoc fac CategoryTheory.Category.comp_id
ofCoconeEquiv_apply_desc 📖	mathematical	—	desc DFunLike.coe Equiv CategoryTheory.Limits.IsColimit CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor EquivLike.toFunLike Equiv.instEquivLike ofCoconeEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unit CategoryTheory.Functor.map descCoconeMorphism CategoryTheory.Equivalence.unitInv	—	—
ofCoconeEquiv_symm_apply_desc 📖	mathematical	—	desc CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor DFunLike.coe Equiv CategoryTheory.Limits.IsColimit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofCoconeEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.map descCoconeMorphism CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counit	—	—
ofIsoColimit_desc 📖	mathematical	—	desc ofIsoColimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Iso.inv CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category	—	—
subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsColimit	—	—
uniq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	desc	—	—
uniq_cocone_morphism 📖	—	—	—	—	CategoryTheory.Limits.CoconeMorphism.ext uniq CategoryTheory.Limits.CoconeMorphism.w
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category uniqueUpToIso descCoconeMorphism	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category uniqueUpToIso descCoconeMorphism	—	—
ι_app_homEquiv_symm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv	—	fac
ι_app_homEquiv_symm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_app_homEquiv_symm
ι_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι map	—	fac
ι_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_map

CategoryTheory.Limits.IsColimit.OfNatIso

Definitions

Name	Category	Theorems
coconeOfHom 📖	CompOp	3 math math: homOfCocone_coconeOfHom, coconeOfHom_homOfCocone, coconeOfHom_fac
colimitCocone 📖	CompOp	2 math math: cocone_fac, coconeOfHom_fac
homOfCocone 📖	CompOp	3 math math: homOfCocone_coconeOfHom, cocone_fac, coconeOfHom_homOfCocone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeOfHom_fac 📖	mathematical	—	coconeOfHom CategoryTheory.Limits.Cocone.extend colimitCocone	—	CategoryTheory.Category.id_comp CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
coconeOfHom_homOfCocone 📖	mathematical	—	coconeOfHom CategoryTheory.Limits.Cocone.pt homOfCocone	—	Equiv.apply_symm_apply
cocone_fac 📖	mathematical	—	CategoryTheory.Limits.Cocone.extend colimitCocone CategoryTheory.Limits.Cocone.pt homOfCocone	—	coconeOfHom_homOfCocone homOfCocone_coconeOfHom coconeOfHom_fac
homOfCocone_coconeOfHom 📖	mathematical	—	homOfCocone coconeOfHom	—	Equiv.symm_apply_apply

CategoryTheory.Limits.IsLimit

Definitions

Name	Category	Theorems
conePointUniqueUpToIso 📖	CompOp	18 math math: conePointUniqueUpToIso_hom_comp_assoc, lift_comp_conePointUniqueUpToIso_hom_assoc, conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.opProductIsoCoproduct'_comp_self, lift_comp_conePointUniqueUpToIso_hom, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv, CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp_assoc, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom, lift_comp_conePointUniqueUpToIso_inv_assoc, lift_comp_conePointUniqueUpToIso_inv, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.Pi.map_eq_prod_map, conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv, conePointUniqueUpToIso_inv_comp_assoc, CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom
conePointsIsoOfEquivalence 📖	CompOp	2 math math: conePointsIsoOfEquivalence_hom, conePointsIsoOfEquivalence_inv
conePointsIsoOfNatIso 📖	CompOp	10 math math: conePointsIsoOfNatIso_hom, conePointsIsoOfNatIso_inv_comp, lift_comp_conePointsIsoOfNatIso_inv, lift_comp_conePointsIsoOfNatIso_hom, conePointsIsoOfNatIso_hom_comp_assoc, conePointsIsoOfNatIso_inv, lift_comp_conePointsIsoOfNatIso_inv_assoc, lift_comp_conePointsIsoOfNatIso_hom_assoc, conePointsIsoOfNatIso_inv_comp_assoc, conePointsIsoOfNatIso_hom_comp
equivIsoLimit 📖	CompOp	2 math math: equivIsoLimit_apply, equivIsoLimit_symm_apply
equivOfNatIsoOfIso 📖	CompOp	—
extendIso 📖	CompOp	—
extendIsoEquiv 📖	CompOp	—
homEquiv 📖	CompOp	4 math math: homEquiv_symm_π_app, homEquiv_symm_π_app_assoc, homEquiv_symm_naturality, homEquiv_apply
homIso 📖	CompOp	1 math math: homIso_hom
homIso' 📖	CompOp	—
isoUniqueConeMorphism 📖	CompOp	—
liftConeMorphism 📖	CompOp	8 math math: ofConeEquiv_symm_apply_desc, liftConeMorphism_eq_isTerminal_from, uniqueUpToIso_inv, liftConeMorphism_hom, ofConeEquiv_apply_desc, uniqueUpToIso_hom, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism
map 📖	CompOp	8 math math: map_π, conePointsIsoOfNatIso_hom, lift_comp_conePointsIsoOfNatIso_inv, lift_comp_conePointsIsoOfNatIso_hom, conePointsIsoOfNatIso_inv, lift_comp_conePointsIsoOfNatIso_inv_assoc, lift_comp_conePointsIsoOfNatIso_hom_assoc, map_π_assoc
mapConeEquiv 📖	CompOp	—
mkConeMorphism 📖	CompOp	1 math math: mkConeMorphism_lift
natIso 📖	CompOp	—
ofConeEquiv 📖	CompOp	2 math math: ofConeEquiv_symm_apply_desc, ofConeEquiv_apply_desc
ofExistsUnique 📖	CompOp	—
ofExtendIso 📖	CompOp	—
ofFaithful 📖	CompOp	—
ofIsoLimit 📖	CompOp	3 math math: equivIsoLimit_apply, ofIsoLimit_lift, equivIsoLimit_symm_apply
ofPointIso 📖	CompOp	—
ofRepresentableBy 📖	CompOp	—
ofRightAdjoint 📖	CompOp	1 math math: CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left
ofWhiskerEquivalence 📖	CompOp	—
postcomposeHomEquiv 📖	CompOp	—
postcomposeInvEquiv 📖	CompOp	—
representableBy 📖	CompOp	—
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_inv, uniqueUpToIso_hom
whiskerEquivalence 📖	CompOp	—
whiskerEquivalenceEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conePointUniqueUpToIso_hom_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.Iso.hom conePointUniqueUpToIso CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.ConeMorphism.w
conePointUniqueUpToIso_hom_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.hom conePointUniqueUpToIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' conePointUniqueUpToIso_hom_comp
conePointUniqueUpToIso_inv_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.Iso.inv conePointUniqueUpToIso CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.ConeMorphism.w
conePointUniqueUpToIso_inv_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.inv conePointUniqueUpToIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' conePointUniqueUpToIso_inv_comp
conePointsIsoOfEquivalence_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cone.pt conePointsIsoOfEquivalence lift CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.Cones.equivalenceOfReindexing CategoryTheory.Equivalence.symm CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Iso.symm CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.Equivalence.invFunIdAssoc	—	—
conePointsIsoOfEquivalence_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cone.pt conePointsIsoOfEquivalence lift CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.Cones.equivalenceOfReindexing	—	—
conePointsIsoOfNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cone.pt conePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	—
conePointsIsoOfNatIso_hom_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.Iso.hom conePointsIsoOfNatIso CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	map_π
conePointsIsoOfNatIso_hom_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.hom conePointsIsoOfNatIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' conePointsIsoOfNatIso_hom_comp
conePointsIsoOfNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cone.pt conePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	—
conePointsIsoOfNatIso_inv_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.Iso.inv conePointsIsoOfNatIso CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	map_π
conePointsIsoOfNatIso_inv_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.inv conePointsIsoOfNatIso CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' conePointsIsoOfNatIso_inv_comp
equivIsoLimit_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Limits.IsLimit EquivLike.toFunLike Equiv.instEquivLike equivIsoLimit ofIsoLimit	—	—
equivIsoLimit_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Limits.IsLimit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivIsoLimit ofIsoLimit CategoryTheory.Iso.symm CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category	—	—
existsUnique 📖	mathematical	—	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	fac uniq
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj lift CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	—
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cone.extend	—	—
homEquiv_symm_naturality 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	Equiv.injective Equiv.apply_symm_apply CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.NatTrans.ext' homEquiv_symm_π_app
homEquiv_symm_π_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.category CategoryTheory.Functor.const EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	fac
homEquiv_symm_π_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homEquiv_symm_π_app
homIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const homIso CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cone.extend	—	—
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	—	hom_lift
hom_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category	—	uniq_cone_morphism
hom_lift 📖	mathematical	—	lift CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	uniq CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.Cone.w
liftConeMorphism_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom liftConeMorphism lift	—	—
lift_comp_conePointUniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.hom conePointUniqueUpToIso	—	uniq CategoryTheory.Category.assoc conePointUniqueUpToIso_hom_comp fac
lift_comp_conePointUniqueUpToIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.hom conePointUniqueUpToIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_conePointUniqueUpToIso_hom
lift_comp_conePointUniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.inv conePointUniqueUpToIso	—	uniq CategoryTheory.Category.assoc conePointUniqueUpToIso_inv_comp fac
lift_comp_conePointUniqueUpToIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.inv conePointUniqueUpToIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_conePointUniqueUpToIso_inv
lift_comp_conePointsIsoOfNatIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.hom conePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	hom_ext CategoryTheory.Category.assoc map_π fac_assoc
lift_comp_conePointsIsoOfNatIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.hom conePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_conePointsIsoOfNatIso_hom
lift_comp_conePointsIsoOfNatIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.inv conePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	hom_ext CategoryTheory.Category.assoc map_π fac_assoc
lift_comp_conePointsIsoOfNatIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt lift CategoryTheory.Iso.inv conePointsIsoOfNatIso map CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_conePointsIsoOfNatIso_inv
lift_self 📖	mathematical	—	lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	uniq CategoryTheory.Category.id_comp
map_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj map CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	fac
map_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt map CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_π
mkConeMorphism_lift 📖	mathematical	—	lift mkConeMorphism CategoryTheory.Limits.ConeMorphism.hom	—	—
nonempty_isLimit_iff_isIso_lift 📖	mathematical	—	CategoryTheory.Limits.IsLimit CategoryTheory.IsIso CategoryTheory.Limits.Cone.pt lift	—	hom_ext CategoryTheory.Category.assoc fac CategoryTheory.Category.id_comp
ofConeEquiv_apply_desc 📖	mathematical	—	lift DFunLike.coe Equiv CategoryTheory.Limits.IsLimit CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor EquivLike.toFunLike Equiv.instEquivLike ofConeEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.id CategoryTheory.Equivalence.inverse CategoryTheory.Functor.comp CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map liftConeMorphism CategoryTheory.Iso.inv	—	—
ofConeEquiv_symm_apply_desc 📖	mathematical	—	lift CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor DFunLike.coe Equiv CategoryTheory.Limits.IsLimit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofConeEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map liftConeMorphism	—	—
ofIsoLimit_lift 📖	mathematical	—	lift ofIsoLimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Iso.hom CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category	—	—
subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsLimit	—	—
uniq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	lift	—	—
uniq_cone_morphism 📖	—	—	—	—	CategoryTheory.Limits.ConeMorphism.ext uniq CategoryTheory.Limits.ConeMorphism.w
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category uniqueUpToIso liftConeMorphism	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category uniqueUpToIso liftConeMorphism	—	—

CategoryTheory.Limits.IsLimit.OfNatIso

Definitions

Name	Category	Theorems
coneOfHom 📖	CompOp	3 math math: coneOfHom_fac, homOfCone_coneOfHom, coneOfHom_homOfCone
homOfCone 📖	CompOp	3 math math: cone_fac, homOfCone_coneOfHom, coneOfHom_homOfCone
limitCone 📖	CompOp	2 math math: cone_fac, coneOfHom_fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneOfHom_fac 📖	mathematical	—	coneOfHom CategoryTheory.Limits.Cone.extend limitCone	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.RepresentableBy.homEquiv_comp
coneOfHom_homOfCone 📖	mathematical	—	coneOfHom CategoryTheory.Limits.Cone.pt homOfCone	—	Equiv.apply_symm_apply
cone_fac 📖	mathematical	—	CategoryTheory.Limits.Cone.extend limitCone CategoryTheory.Limits.Cone.pt homOfCone	—	coneOfHom_homOfCone homOfCone_coneOfHom coneOfHom_fac
homOfCone_coneOfHom 📖	mathematical	—	homOfCone coneOfHom	—	Equiv.symm_apply_apply

---

← Back to Index