Elements

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

Statistics

Metric	Count
Definitions isLimit, isValidLift, liftedCone, liftedConeElement, liftedConeElement', instCreatesLimitElementsπ, instCreatesLimitsOfShapeElementsπ, Elements, Elements	9
Theorems liftedCone_pt_fst, liftedCone_pt_snd, liftedCone_π_app_coe, map_lift_mapCone, map_π_liftedConeElement, π_liftedConeElement', instHasInitialElementsOfIsCorepresentable, instHasInitialElementsOppositeOfIsRepresentable, instHasLimitsOfShapeElements	9
Total	18

CategoryTheory.CategoryOfElements

Definitions

Name	Category	Theorems
instCreatesLimitElementsπ 📖	CompOp	—
instCreatesLimitsOfShapeElementsπ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasInitialElementsOfIsCorepresentable 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements	—	CategoryTheory.Limits.IsInitial.hasInitial
instHasInitialElementsOppositeOfIsRepresentable 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.Functor.Elements Opposite CategoryTheory.Category.opposite CategoryTheory.categoryOfElements	—	CategoryTheory.Limits.IsInitial.hasInitial
instHasLimitsOfShapeElements 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements	—	CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape

CategoryTheory.CategoryOfElements.CreatesLimitsAux

Definitions

Name	Category	Theorems
isLimit 📖	CompOp	—
isValidLift 📖	CompOp	—
liftedCone 📖	CompOp	3 math math: liftedCone_π_app_coe, liftedCone_pt_snd, liftedCone_pt_fst
liftedConeElement 📖	CompOp	4 math math: liftedCone_π_app_coe, liftedCone_pt_snd, map_lift_mapCone, map_π_liftedConeElement
liftedConeElement' 📖	CompOp	1 math math: π_liftedConeElement'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftedCone_pt_fst 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements liftedCone CategoryTheory.Limits.limit CategoryTheory.Functor.comp CategoryTheory.CategoryOfElements.π	—	—
liftedCone_pt_snd 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements liftedCone liftedConeElement	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
liftedCone_π_app_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.limit CategoryTheory.Functor.comp CategoryTheory.CategoryOfElements.π liftedConeElement CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π liftedCone CategoryTheory.Limits.limit.π	—	—
map_lift_mapCone 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.CategoryOfElements.π CategoryTheory.Functor.mapCone CategoryTheory.Limits.limit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.limit.lift CategoryTheory.Functor.obj liftedConeElement	—	Equiv.injective CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.Types.limit_ext CategoryTheory.preservesLimitIso_hom_π CategoryTheory.Limits.limit.lift_π CategoryTheory.inv_hom_id_apply π_liftedConeElement'
map_π_liftedConeElement 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.Limits.limit CategoryTheory.Functor.comp CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.CategoryOfElements.π CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.obj CategoryTheory.Limits.limit.π liftedConeElement	—	CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.preservesLimitIso_inv_π π_liftedConeElement'
π_liftedConeElement' 📖	mathematical	—	CategoryTheory.Limits.limit.π CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.CategoryOfElements.π CategoryTheory.Limits.Types.hasLimit liftedConeElement' CategoryTheory.Functor.obj	—	CategoryTheory.Limits.Types.hasLimit

CategoryTheory.Functor

Definitions

Name	Category	Theorems
Elements 📖	CompOp	112 math math: CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElements, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app, CategoryTheory.CategoryOfElements.fromStructuredArrow_map, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instIsCofilteredElementsFiber, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_functor, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_functor, Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc, CategoryTheory.Presheaf.coconeOfRepresentable_pt, CategoryTheory.CategoryOfElements.map_map_coe, CategoryTheory.Presheaf.functorToRepresentables_map, SSet.S.equivElements_symm_apply_dim, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base, CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe, Elements.coconeπOpCompShrinkYonedaObj_pt, CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, CategoryTheory.CategoryOfElements.to_comma_map_right, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso, CategoryTheory.CategoryOfElements.instHasInitialElementsOppositeOfIsRepresentable, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_π_app_coe, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base, CategoryTheory.CategoryOfElements.toStructuredArrow_obj, CategoryTheory.CategoryOfElements.map_π, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst, CategoryTheory.CategoryOfElements.isoMk_inv, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base, CategoryTheory.Presheaf.functorToRepresentables_obj, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_map, CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_pt, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso, CategoryTheory.CategoryOfElements.comp_val, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse, CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe, CategoryTheory.CategoryOfElements.fromStructuredArrow_obj, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_obj, CategoryTheory.CategoryOfElements.instFaithfulElementsπ, CategoryTheory.NatTrans.mapElements_map_coe, CategoryTheory.CategoryOfElements.map_obj_fst, CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_snd, CategoryTheory.instIsCofilteredElementsCompOfRepresentablyFlat, CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse, CategoryTheory.CategoryOfElements.map_obj_snd, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_obj_fst, CategoryTheory.CategoryOfElements.instReflectsIsomorphismsElementsπ, Elements.instHasInitialObjOppositeTypeFlipShrinkYonedaOp, elementsFunctor_map, CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_obj_snd, CategoryTheory.CategoryOfElements.π_map, isCofiltered_elements, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitialElementsFiberFunctorOfIsCofiltered, CategoryTheory.CategoryOfElements.fromCostructuredArrow_map_coe, SSet.S.equivElements_apply_fst, CategoryTheory.CategoryOfElements.instLocallySmallElements, CategoryTheory.CategoryOfElements.instHasInitialElementsOfIsCorepresentable, CategoryTheory.CategoryOfElements.π_obj, CategoryTheory.NatTrans.mapElements_obj, CategoryTheory.GrothendieckTopology.Point.instIsSiftedOppositeElementsFiber, CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, CategoryTheory.CategoryOfElements.toCostructuredArrow_obj, CategoryTheory.Presheaf.coconeOfRepresentable_naturality, CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ι_app, CategoryTheory.GrothendieckTopology.Point.instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits, Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app, Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app, CategoryTheory.GrothendieckTopology.Point.instHasColimitsOfShapeOppositeElementsFiber, CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj, elementsFunctor_obj, SSet.S.equivElements_apply_snd, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as, SSet.S.le_iff_nonempty_hom, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso, CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor, SSet.S.equivElements_symm_apply_simplex, CategoryTheory.Presheaf.coconeOfRepresentable_ι_app, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app, CategoryTheory.CategoryOfElements.id_val, Elements.coconeπOpCompShrinkYonedaObj_ι_app, CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberForget, CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_mk, CategoryTheory.GrothendieckTopology.Point.map_aux, CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_ι_app, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_snd, CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitiallySmallElementsFiberOfIsCofiltered, CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone, CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base, CategoryTheory.FunctorToTypes.instIsCofilteredElementsOverFromOverFunctor, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe, CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement, CategoryTheory.GrothendieckTopology.Point.isCofiltered, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map, CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as, CategoryTheory.CategoryOfElements.isoMk_hom, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_fst, CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_fst, CategoryTheory.CategoryOfElements.toCostructuredArrow_map, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app, CategoryTheory.CategoryOfElements.CreatesLimitsAux.π_liftedConeElement', CategoryTheory.GrothendieckTopology.Point.initiallySmall, CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_pt

PresheafOfModules

Definitions

Name	Category	Theorems
Elements 📖	CompOp	—

---

← Back to Index