Elements

📁 Source: Mathlib/CategoryTheory/Elements.lean

Statistics

Metric	Count
Definitions costructuredArrowULiftYonedaEquivalence, costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso, costructuredArrowYonedaEquivalence, costructuredArrowYonedaEquivalenceFunctorProj, costructuredArrowYonedaEquivalenceInverseπ, fromCostructuredArrow, fromStructuredArrow, homMk, isoMk, map, structuredArrowEquivalence, toCostructuredArrow, toStructuredArrow, π, initial, initialOfCorepresentableBy, initialOfRepresentableBy, isInitial, isInitialOfCorepresentableBy, isInitialOfRepresentableBy, elementsFunctor, elementsMk, mapElements, categoryOfElements, groupoidOfElements	25
Theorems comp_val, costructuredArrowULiftYonedaEquivalence_counitIso, costructuredArrowULiftYonedaEquivalence_functor_map, costructuredArrowULiftYonedaEquivalence_functor_obj, costructuredArrowULiftYonedaEquivalence_inverse_map, costructuredArrowULiftYonedaEquivalence_inverse_obj, costructuredArrowULiftYonedaEquivalence_unitIso, costructuredArrowYonedaEquivalenceFunctorProj_hom_app, costructuredArrowYonedaEquivalenceFunctorProj_inv_app, costructuredArrowYonedaEquivalenceInverseπ_hom_app, costructuredArrowYonedaEquivalenceInverseπ_inv_app, costructuredArrowYonedaEquivalence_counitIso, costructuredArrowYonedaEquivalence_functor, costructuredArrowYonedaEquivalence_inverse, costructuredArrowYonedaEquivalence_unitIso, costructuredArrow_yoneda_equivalence_naturality, ext, ext_iff, fromCostructuredArrow_map_coe, fromCostructuredArrow_obj_fst, fromCostructuredArrow_obj_mk, fromCostructuredArrow_obj_snd, fromStructuredArrow_map, fromStructuredArrow_obj, homMk_coe, id_val, instFaithfulElementsπ, instLocallySmallElements, instReflectsIsomorphismsElementsπ, isoMk_hom, isoMk_inv, map_map_coe, map_obj_fst, map_obj_snd, map_snd, map_π, structuredArrowEquivalence_counitIso, structuredArrowEquivalence_functor, structuredArrowEquivalence_inverse, structuredArrowEquivalence_unitIso, toCostructuredArrow_map, toCostructuredArrow_obj, toStructuredArrow_obj, to_comma_map_right, π_map, π_obj, ext, initialOfCorepresentableBy_fst, initialOfCorepresentableBy_snd, initialOfRepresentableBy_fst, initialOfRepresentableBy_snd, elementsFunctor_map, elementsFunctor_obj, mapElements_map_coe, mapElements_obj	55
Total	80

CategoryTheory

Definitions

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

CategoryTheory.CategoryOfElements

Definitions

Name	Category	Theorems
costructuredArrowULiftYonedaEquivalence 📖	CompOp	6 math math: costructuredArrowULiftYonedaEquivalence_unitIso, costructuredArrowULiftYonedaEquivalence_functor_obj, costructuredArrowULiftYonedaEquivalence_functor_map, costructuredArrowULiftYonedaEquivalence_counitIso, costructuredArrowULiftYonedaEquivalence_inverse_obj, costructuredArrowULiftYonedaEquivalence_inverse_map
costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso 📖	CompOp	—
costructuredArrowYonedaEquivalence 📖	CompOp	8 math math: costructuredArrowYonedaEquivalenceInverseπ_hom_app, costructuredArrowYonedaEquivalence_functor, costructuredArrowYonedaEquivalence_counitIso, costructuredArrowYonedaEquivalence_inverse, costructuredArrowYonedaEquivalence_unitIso, costructuredArrowYonedaEquivalenceFunctorProj_hom_app, costructuredArrowYonedaEquivalenceInverseπ_inv_app, costructuredArrowYonedaEquivalenceFunctorProj_inv_app
costructuredArrowYonedaEquivalenceFunctorProj 📖	CompOp	2 math math: costructuredArrowYonedaEquivalenceFunctorProj_hom_app, costructuredArrowYonedaEquivalenceFunctorProj_inv_app
costructuredArrowYonedaEquivalenceInverseπ 📖	CompOp	2 math math: costructuredArrowYonedaEquivalenceInverseπ_hom_app, costructuredArrowYonedaEquivalenceInverseπ_inv_app
fromCostructuredArrow 📖	CompOp	7 math math: costructuredArrowYonedaEquivalence_counitIso, costructuredArrowYonedaEquivalence_inverse, fromCostructuredArrow_obj_snd, fromCostructuredArrow_map_coe, costructuredArrowYonedaEquivalence_unitIso, fromCostructuredArrow_obj_mk, fromCostructuredArrow_obj_fst
fromStructuredArrow 📖	CompOp	4 math math: fromStructuredArrow_map, structuredArrowEquivalence_counitIso, fromStructuredArrow_obj, structuredArrowEquivalence_inverse
homMk 📖	CompOp	7 math math: costructuredArrowULiftYonedaEquivalence_unitIso, homMk_coe, isoMk_inv, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_map, costructuredArrowULiftYonedaEquivalence_counitIso, costructuredArrowULiftYonedaEquivalence_inverse_map, isoMk_hom
isoMk 📖	CompOp	4 math math: costructuredArrowULiftYonedaEquivalence_unitIso, isoMk_inv, costructuredArrowYonedaEquivalence_unitIso, isoMk_hom
map 📖	CompOp	6 math math: map_map_coe, map_π, map_obj_fst, map_obj_snd, costructuredArrow_yoneda_equivalence_naturality, CategoryTheory.Presheaf.coconeOfRepresentable_naturality
structuredArrowEquivalence 📖	CompOp	4 math math: structuredArrowEquivalence_functor, structuredArrowEquivalence_counitIso, structuredArrowEquivalence_inverse, structuredArrowEquivalence_unitIso
toCostructuredArrow 📖	CompOp	6 math math: costructuredArrowYonedaEquivalence_functor, costructuredArrowYonedaEquivalence_counitIso, costructuredArrow_yoneda_equivalence_naturality, costructuredArrowYonedaEquivalence_unitIso, toCostructuredArrow_obj, toCostructuredArrow_map
toStructuredArrow 📖	CompOp	4 math math: structuredArrowEquivalence_functor, to_comma_map_right, structuredArrowEquivalence_counitIso, toStructuredArrow_obj
π 📖	CompOp	24 math math: costructuredArrowYonedaEquivalenceInverseπ_hom_app, CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc, CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj_pt, CreatesLimitsAux.liftedCone_π_app_coe, map_π, CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_pt, instFaithfulElementsπ, instReflectsIsomorphismsElementsπ, π_map, π_obj, CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ι_app, CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app, CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply, costructuredArrowYonedaEquivalenceFunctorProj_hom_app, CategoryTheory.Presheaf.coconeOfRepresentable_ι_app, costructuredArrowYonedaEquivalenceInverseπ_inv_app, CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj_ι_app, CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_ι_app, CreatesLimitsAux.map_lift_mapCone, CreatesLimitsAux.map_π_liftedConeElement, CreatesLimitsAux.liftedCone_pt_fst, costructuredArrowYonedaEquivalenceFunctorProj_inv_app, CreatesLimitsAux.π_liftedConeElement', CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_pt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_val 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements	—	—
costructuredArrowULiftYonedaEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.categoryOfElements CategoryTheory.instCategoryCostructuredArrow costructuredArrowULiftYonedaEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp Opposite.op CategoryTheory.Functor.elementsMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv CategoryTheory.Comma.hom Quiver.Hom.op homMk CategoryTheory.CommaMorphism.left Opposite.unop Equiv.symm CategoryTheory.CostructuredArrow.homMk Quiver.Hom.unop CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.CostructuredArrow.isoMk CategoryTheory.Iso.refl	—	—
costructuredArrowULiftYonedaEquivalence_functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Equivalence.functor costructuredArrowULiftYonedaEquivalence CategoryTheory.CostructuredArrow.homMk Opposite.unop DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv Quiver.Hom.unop	—	—
costructuredArrowULiftYonedaEquivalence_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Equivalence.functor costructuredArrowULiftYonedaEquivalence Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv	—	—
costructuredArrowULiftYonedaEquivalence_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Equivalence.inverse costructuredArrowULiftYonedaEquivalence Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.elementsMk Opposite.op CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv CategoryTheory.Comma.hom homMk CategoryTheory.CommaMorphism.left	—	—
costructuredArrowULiftYonedaEquivalence_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Equivalence.inverse costructuredArrowULiftYonedaEquivalence Opposite.op CategoryTheory.Functor.elementsMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv CategoryTheory.Comma.hom	—	—
costructuredArrowULiftYonedaEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.categoryOfElements CategoryTheory.instCategoryCostructuredArrow costructuredArrowULiftYonedaEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp Opposite.unop DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv CategoryTheory.CostructuredArrow.homMk Quiver.Hom.unop CategoryTheory.Functor.map CategoryTheory.Functor.elementsMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom Quiver.Hom.op homMk CategoryTheory.CommaMorphism.left CategoryTheory.Iso.op isoMk CategoryTheory.Iso.refl	—	—
costructuredArrowYonedaEquivalenceFunctorProj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Equivalence.functor costructuredArrowYonedaEquivalence CategoryTheory.CostructuredArrow.proj CategoryTheory.Iso.hom CategoryTheory.Functor.leftOp π costructuredArrowYonedaEquivalenceFunctorProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.unop	—	—
costructuredArrowYonedaEquivalenceFunctorProj_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Equivalence.functor costructuredArrowYonedaEquivalence CategoryTheory.CostructuredArrow.proj CategoryTheory.Iso.inv CategoryTheory.Functor.leftOp π costructuredArrowYonedaEquivalenceFunctorProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.unop	—	—
costructuredArrowYonedaEquivalenceInverseπ_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Equivalence.inverse costructuredArrowYonedaEquivalence CategoryTheory.Functor.leftOp π CategoryTheory.Iso.hom CategoryTheory.CostructuredArrow.proj costructuredArrowYonedaEquivalenceInverseπ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
costructuredArrowYonedaEquivalenceInverseπ_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Equivalence.inverse costructuredArrowYonedaEquivalence CategoryTheory.Functor.leftOp π CategoryTheory.Iso.inv CategoryTheory.CostructuredArrow.proj costructuredArrowYonedaEquivalenceInverseπ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
costructuredArrowYonedaEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.categoryOfElements CategoryTheory.instCategoryCostructuredArrow costructuredArrowYonedaEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp CategoryTheory.Functor.rightOp fromCostructuredArrow toCostructuredArrow CategoryTheory.Functor.id CategoryTheory.CostructuredArrow.isoMk CategoryTheory.Functor.obj CategoryTheory.Iso.refl CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
costructuredArrowYonedaEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.categoryOfElements CategoryTheory.instCategoryCostructuredArrow costructuredArrowYonedaEquivalence toCostructuredArrow	—	—
costructuredArrowYonedaEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.categoryOfElements CategoryTheory.instCategoryCostructuredArrow costructuredArrowYonedaEquivalence CategoryTheory.Functor.rightOp fromCostructuredArrow	—	—
costructuredArrowYonedaEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.categoryOfElements CategoryTheory.instCategoryCostructuredArrow costructuredArrowYonedaEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp toCostructuredArrow CategoryTheory.Functor.rightOp fromCostructuredArrow CategoryTheory.Iso.op CategoryTheory.Functor.obj Opposite.op Opposite.unop isoMk CategoryTheory.Iso.refl	—	—
costructuredArrow_yoneda_equivalence_naturality 📖	mathematical	—	CategoryTheory.Functor.comp Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.op map toCostructuredArrow CategoryTheory.CostructuredArrow.map	—	CategoryTheory.Functor.ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.NatTrans.naturality CategoryTheory.CostructuredArrow.eqToHom_left CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
ext 📖	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.map	—	—	—
ext_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.map	—	ext
fromCostructuredArrow_map_coe 📖	mathematical	—	Quiver.Hom Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.types Opposite.op CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.CostructuredArrow Equiv.toFun CategoryTheory.yonedaEquiv CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements fromCostructuredArrow Quiver.Hom.op CategoryTheory.CommaMorphism.left Quiver.Hom.unop	—	—
fromCostructuredArrow_obj_fst 📖	mathematical	—	Opposite CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements fromCostructuredArrow Opposite.op CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop	—	—
fromCostructuredArrow_obj_mk 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements fromCostructuredArrow Opposite.op Equiv.toFun Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.yonedaEquiv	—	—
fromCostructuredArrow_obj_snd 📖	mathematical	—	Opposite CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements fromCostructuredArrow Equiv.toFun Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop Opposite.op CategoryTheory.yonedaEquiv CategoryTheory.Comma.hom	—	—
fromStructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.types CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements fromStructuredArrow Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.w	—	—
fromStructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.types CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements fromStructuredArrow CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom	—	—
homMk_coe 📖	mathematical	CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.Functor.obj	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.map homMk	—	—
id_val 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements	—	—
instFaithfulElementsπ 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements π	—	ext
instLocallySmallElements 📖	mathematical	—	CategoryTheory.LocallySmall CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements	—	small_of_injective CategoryTheory.instSmallHomOfLocallySmall ext
instReflectsIsomorphismsElementsπ 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements π	—	map_snd CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.IsIso.hom_inv_id CategoryTheory.FunctorToTypes.map_id_apply ext CategoryTheory.IsIso.inv_hom_id
isoMk_hom 📖	mathematical	CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Iso.hom	CategoryTheory.Iso.hom CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements isoMk homMk CategoryTheory.Functor.obj CategoryTheory.types	—	—
isoMk_inv 📖	mathematical	CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements isoMk homMk CategoryTheory.Functor.obj CategoryTheory.types	—	—
map_map_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements map	—	—
map_obj_fst 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements map	—	—
map_obj_snd 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements map CategoryTheory.NatTrans.app	—	—
map_snd 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
map_π 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements map π	—	—
structuredArrowEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.Elements CategoryTheory.StructuredArrow CategoryTheory.types CategoryTheory.categoryOfElements CategoryTheory.instCategoryStructuredArrow structuredArrowEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp fromStructuredArrow toStructuredArrow	—	—
structuredArrowEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Functor.Elements CategoryTheory.StructuredArrow CategoryTheory.types CategoryTheory.categoryOfElements CategoryTheory.instCategoryStructuredArrow structuredArrowEquivalence toStructuredArrow	—	—
structuredArrowEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Functor.Elements CategoryTheory.StructuredArrow CategoryTheory.types CategoryTheory.categoryOfElements CategoryTheory.instCategoryStructuredArrow structuredArrowEquivalence fromStructuredArrow	—	—
structuredArrowEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.Elements CategoryTheory.StructuredArrow CategoryTheory.types CategoryTheory.categoryOfElements CategoryTheory.instCategoryStructuredArrow structuredArrowEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
toCostructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.homMk Opposite.unop DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.yonedaEquiv Quiver.Hom.unop	—	—
toCostructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Functor.Elements CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.yonedaEquiv	—	—
toStructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.StructuredArrow CategoryTheory.types CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
to_comma_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.types CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
π_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types	—	—
π_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements π CategoryTheory.types	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
elementsFunctor 📖	CompOp	2 math math: elementsFunctor_map, elementsFunctor_obj
elementsMk 📖	CompOp	5 math math: CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_map, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elementsFunctor_map 📖	mathematical	—	map CategoryTheory.Functor CategoryTheory.types category CategoryTheory.Cat CategoryTheory.Cat.category elementsFunctor toCatHom Elements CategoryTheory.categoryOfElements CategoryTheory.NatTrans.mapElements	—	—
elementsFunctor_obj 📖	mathematical	—	obj CategoryTheory.Functor CategoryTheory.types category CategoryTheory.Cat CategoryTheory.Cat.category elementsFunctor CategoryTheory.Cat.of Elements CategoryTheory.categoryOfElements	—	—

CategoryTheory.Functor.Elements

Definitions

Name	Category	Theorems
initial 📖	CompOp	—
initialOfCorepresentableBy 📖	CompOp	2 math math: initialOfCorepresentableBy_snd, initialOfCorepresentableBy_fst
initialOfRepresentableBy 📖	CompOp	2 math math: initialOfRepresentableBy_snd, initialOfRepresentableBy_fst
isInitial 📖	CompOp	—
isInitialOfCorepresentableBy 📖	CompOp	—
isInitialOfRepresentableBy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.FunctorToTypes.map_id_apply
initialOfCorepresentableBy_fst 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types initialOfCorepresentableBy	—	—
initialOfCorepresentableBy_snd 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types initialOfCorepresentableBy DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.CategoryStruct.id	—	—
initialOfRepresentableBy_fst 📖	mathematical	—	Opposite CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.types initialOfRepresentableBy Opposite.op	—	—
initialOfRepresentableBy_snd 📖	mathematical	—	Opposite CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.types initialOfRepresentableBy DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.RepresentableBy.homEquiv CategoryTheory.CategoryStruct.id	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
mapElements 📖	CompOp	4 math math: mapElements_map_coe, CategoryTheory.Functor.elementsFunctor_map, mapElements_obj, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapElements_map_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.Elements app CategoryTheory.Functor.map CategoryTheory.categoryOfElements mapElements	—	—
mapElements_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements mapElements CategoryTheory.types app	—	—

---

← Back to Index