Yoneda

📁 Source: Mathlib/Topology/Category/TopCat/Yoneda.lean

Statistics

Metric	Count
Definitions yonedaPresheaf, yonedaPresheaf'	2
Theorems comp_yonedaPresheaf', instPreservesFiniteProductsOppositeTopCatYonedaPresheaf', piComparison_fac, yonedaPresheaf'_map, yonedaPresheaf'_obj, yonedaPresheaf_map, yonedaPresheaf_obj	7
Total	9

ContinuousMap

Definitions

Name	Category	Theorems
yonedaPresheaf 📖	CompOp	5 math math: equalizerCondition_yonedaPresheaf, yonedaPresheaf_map, yonedaPresheaf_obj, instPreservesFiniteProductsOppositeYonedaPresheafOfPreservesFiniteCoproductsTopCat, comp_yonedaPresheaf'
yonedaPresheaf' 📖	CompOp	5 math math: yonedaPresheaf'_obj, piComparison_fac, yonedaPresheaf'_map, comp_yonedaPresheaf', instPreservesFiniteProductsOppositeTopCatYonedaPresheaf'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_yonedaPresheaf' 📖	mathematical	—	yonedaPresheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite TopCat TopCat.instCategory CategoryTheory.types CategoryTheory.Functor.op yonedaPresheaf'	—	—
instPreservesFiniteProductsOppositeTopCatYonedaPresheaf' 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts Opposite TopCat CategoryTheory.Category.opposite TopCat.instCategory CategoryTheory.types yonedaPresheaf'	—	CategoryTheory.Limits.PreservesProduct.of_iso_comparison CategoryTheory.Limits.instHasProductOppositeOp CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.Types.hasLimit piComparison_fac CategoryTheory.IsIso.comp_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.isIso_op CategoryTheory.Limits.preservesLimit_of_iso_diagram
piComparison_fac 📖	mathematical	—	CategoryTheory.Limits.piComparison Opposite TopCat CategoryTheory.Category.opposite TopCat.instCategory CategoryTheory.types yonedaPresheaf' Opposite.op CategoryTheory.Limits.instHasProductOppositeOp CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Discrete.functor CategoryTheory.Limits.Types.hasLimit CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.piObj TopCat.of TopCat.carrier instTopologicalSpaceSigma TopCat.str ContinuousMap CategoryTheory.Functor.map CategoryTheory.CategoryStruct.opposite CategoryTheory.Limits.sigmaObj CategoryTheory.Iso.inv CategoryTheory.Limits.opCoproductIsoProduct Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver TopCat.sigmaIsoSigma DFunLike.coe Equiv CategoryTheory.Iso EquivLike.toFunLike Equiv.instEquivLike equivEquivIso sigmaEquiv CategoryTheory.Limits.Types.productIso	—	CategoryTheory.Limits.instHasProductOppositeOp CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.Types.hasLimit CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv CategoryTheory.types_ext ext CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply CategoryTheory.Limits.Types.pi_lift_π_apply
yonedaPresheaf'_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopCat CategoryTheory.Category.opposite TopCat.instCategory CategoryTheory.types yonedaPresheaf' comp TopCat.carrier Opposite.unop TopCat.str CategoryTheory.ConcreteCategory.hom ContinuousMap instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
yonedaPresheaf'_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopCat CategoryTheory.Category.opposite TopCat.instCategory CategoryTheory.types yonedaPresheaf' ContinuousMap TopCat.carrier Opposite.unop TopCat.str	—	—
yonedaPresheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types yonedaPresheaf comp TopCat.carrier CategoryTheory.Functor.obj TopCat TopCat.instCategory Opposite.unop TopCat.str TopCat.Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
yonedaPresheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types yonedaPresheaf ContinuousMap TopCat.carrier TopCat TopCat.instCategory Opposite.unop TopCat.str	—	—

---

← Back to Index