Subcanonical

📁 Source: Mathlib/CategoryTheory/Sites/Subcanonical.lean

Statistics

Metric	Count
Definitions Subcanonical, isColimitCofanMkYoneda, uliftYonedaEquiv, uliftYonedaOpCompCoyoneda, yonedaEquiv, yonedaOpCompCoyoneda, yonedaULiftEquiv	7
Theorems hom_ext_uliftYoneda, hom_ext_yoneda, hom_ext_yonedaULift, map_uliftYonedaEquiv, map_uliftYonedaEquiv', map_yonedaEquiv, map_yonedaEquiv', map_yonedaULiftEquiv, map_yonedaULiftEquiv', preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem, preservesLimitsOfSize_yoneda, subcanonical_of_full_of_faithful, uliftYonedaEquiv_apply, uliftYonedaEquiv_comp, uliftYonedaEquiv_naturality, uliftYonedaEquiv_naturality', uliftYonedaEquiv_symm_app_apply, uliftYonedaEquiv_symm_map, uliftYonedaEquiv_symm_naturality_left, uliftYonedaEquiv_symm_naturality_right, uliftYonedaEquiv_uliftYoneda_map, uliftYonedaOpCompCoyoneda_app_app, uliftYonedaOpCompCoyoneda_hom_app_app_down, uliftYonedaOpCompCoyoneda_inv_app_app, uliftYonedaOpCompCoyoneda_inv_app_app_hom_app, yonedaEquiv_apply, yonedaEquiv_comp, yonedaEquiv_naturality, yonedaEquiv_naturality', yonedaEquiv_symm_app_apply, yonedaEquiv_symm_map, yonedaEquiv_symm_naturality_left, yonedaEquiv_symm_naturality_right, yonedaEquiv_yoneda_map, yonedaOpCompCoyoneda_hom_app_app_down, yonedaOpCompCoyoneda_inv_app_app, yonedaULiftEquiv_apply, yonedaULiftEquiv_comp, yonedaULiftEquiv_naturality, yonedaULiftEquiv_naturality', yonedaULiftEquiv_symm_app_apply, yonedaULiftEquiv_symm_map, yonedaULiftEquiv_symm_naturality_left, yonedaULiftEquiv_symm_naturality_right, yonedaULiftEquiv_yonedaULift_map	45
Total	52

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
Subcanonical 📖	CompData	15 math math: AlgebraicGeometry.Scheme.instSubcanonicalFppfTopology, subcanonical_over, subcanonical_of_full_of_faithful, CategoryTheory.regularTopology.subcanonical, CategoryTheory.extensiveTopology.subcanonical, AlgebraicGeometry.Scheme.ProEt.instSubcanonicalTopology, CategoryTheory.coherentTopology.subcanonical, AlgebraicGeometry.Scheme.instSubcanonicalFpqcTopology, Subcanonical.of_le, instSubcanonicalCanonicalTopology, Subcanonical.of_isSheaf_yoneda_obj, CategoryTheory.subcanonical_typesGrothendieckTopology, AlgebraicGeometry.Scheme.instSubcanonicalProetaleTopology, TopCat.subcanonical_grothendieckTopology, AlgebraicGeometry.Scheme.subcanonical_zariskiTopology
isColimitCofanMkYoneda 📖	CompOp	—
uliftYonedaEquiv 📖	CompOp	24 math math: yonedaULiftEquiv_apply, uliftYonedaEquiv_naturality, uliftYonedaEquiv_naturality', uliftYonedaEquiv_symm_map, yonedaULiftEquiv_naturality', yonedaULiftEquiv_symm_naturality_left, yonedaULiftEquiv_symm_naturality_right, uliftYonedaEquiv_uliftYoneda_map, uliftYonedaEquiv_symm_app_apply, map_uliftYonedaEquiv', map_yonedaULiftEquiv', uliftYonedaEquiv_apply, uliftYonedaEquiv_symm_naturality_left, uliftYonedaOpCompCoyoneda_app_app, yonedaULiftEquiv_naturality, map_uliftYonedaEquiv, uliftYonedaOpCompCoyoneda_inv_app_app, yonedaULiftEquiv_comp, yonedaULiftEquiv_symm_app_apply, yonedaULiftEquiv_symm_map, uliftYonedaEquiv_symm_naturality_right, yonedaULiftEquiv_yonedaULift_map, map_yonedaULiftEquiv, uliftYonedaEquiv_comp
uliftYonedaOpCompCoyoneda 📖	CompOp	4 math math: uliftYonedaOpCompCoyoneda_hom_app_app_down, uliftYonedaOpCompCoyoneda_app_app, uliftYonedaOpCompCoyoneda_inv_app_app, uliftYonedaOpCompCoyoneda_inv_app_app_hom_app
yonedaEquiv 📖	CompOp	13 math math: LightCondensed.ihomPoints_apply, yonedaEquiv_symm_app_apply, yonedaEquiv_naturality', map_yonedaEquiv', yonedaEquiv_comp, yonedaEquiv_symm_map, yonedaEquiv_naturality, LightCondensed.ihomPoints_symm_apply, yonedaEquiv_symm_naturality_left, map_yonedaEquiv, yonedaEquiv_yoneda_map, yonedaEquiv_apply, yonedaEquiv_symm_naturality_right
yonedaOpCompCoyoneda 📖	CompOp	2 math math: yonedaOpCompCoyoneda_hom_app_app_down, yonedaOpCompCoyoneda_inv_app_app
yonedaULiftEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext_uliftYoneda 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda	—	—	CategoryTheory.ObjectProperty.hom_ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext Equiv.apply_symm_apply
hom_ext_yoneda 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj yoneda	—	—	CategoryTheory.ObjectProperty.hom_ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext Equiv.apply_symm_apply
hom_ext_yonedaULift 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda	—	—	hom_ext_uliftYoneda
map_uliftYonedaEquiv 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.sheafToPresheaf yoneda	—	uliftYonedaEquiv_naturality uliftYonedaEquiv_comp uliftYonedaEquiv_uliftYoneda_map
map_uliftYonedaEquiv' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.sheafToPresheaf yoneda Quiver.Hom.unop	—	uliftYonedaEquiv_naturality' uliftYonedaEquiv_comp uliftYonedaEquiv_uliftYoneda_map
map_yonedaEquiv 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj yoneda EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	yonedaEquiv_naturality yonedaEquiv_comp yonedaEquiv_yoneda_map
map_yonedaEquiv' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj yoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.unop	—	yonedaEquiv_naturality' yonedaEquiv_comp yonedaEquiv_yoneda_map
map_yonedaULiftEquiv 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.sheafToPresheaf yoneda	—	map_uliftYonedaEquiv
map_yonedaULiftEquiv' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.sheafToPresheaf yoneda Quiver.Hom.unop	—	map_uliftYonedaEquiv'
preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem 📖	mathematical	CategoryTheory.Sieve CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Discrete CategoryTheory.discreteCategory yoneda	—	CategoryTheory.Limits.preservesColimitsOfShape_of_discrete CategoryTheory.Mono.of_coproductDisjoint CategoryTheory.Limits.CoproductsOfShapeDisjoint.coproductDisjoint CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks
preservesLimitsOfSize_yoneda 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf yoneda	—	CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
subcanonical_of_full_of_faithful 📖	mathematical	—	Subcanonical	—	Subcanonical.of_isSheaf_yoneda_obj CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.Presheaf.isSheaf_of_iso_iff CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf Subcanonical.isSheaf_of_isRepresentable CategoryTheory.Functor.instIsRepresentableObjOppositeTypeUliftYoneda CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv
uliftYonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.sheafToPresheaf yoneda CategoryTheory.CategoryStruct.id	—	—
uliftYonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—
uliftYonedaEquiv_naturality 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp	—	CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
uliftYonedaEquiv_naturality' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	uliftYonedaEquiv_naturality
uliftYonedaEquiv_symm_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category uliftYoneda CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.sheafToPresheaf yoneda CategoryTheory.Functor.map Opposite.unop Quiver.Hom.op	—	—
uliftYonedaEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Opposite.unop Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category uliftYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	Equiv.surjective uliftYonedaEquiv_naturality' Equiv.symm_apply_apply
uliftYonedaEquiv_symm_naturality_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.Functor.map DFunLike.coe Equiv CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv Quiver.Hom.op	—	Equiv.injective Equiv.apply_symm_apply uliftYonedaEquiv_uliftYoneda_map
uliftYonedaEquiv_symm_naturality_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda DFunLike.coe Equiv CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	Equiv.injective Equiv.apply_symm_apply
uliftYonedaEquiv_uliftYoneda_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.Functor.map CategoryTheory.sheafToPresheaf yoneda	—	uliftYonedaEquiv_apply CategoryTheory.Category.id_comp
uliftYonedaOpCompCoyoneda_app_app 📖	mathematical	—	CategoryTheory.Iso.app CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.op uliftYoneda CategoryTheory.coyoneda CategoryTheory.evaluation CategoryTheory.Functor.whiskeringRight CategoryTheory.uliftFunctor CategoryTheory.Functor.whiskeringLeft CategoryTheory.sheafToPresheaf uliftYonedaOpCompCoyoneda Equiv.toIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Equiv.trans uliftYonedaEquiv Equiv.symm Equiv.ulift	—	—
uliftYonedaOpCompCoyoneda_hom_app_app_down 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.evaluation CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.op yoneda CategoryTheory.sheafCompose CategoryTheory.uliftFunctor CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.hom uliftYoneda uliftYonedaOpCompCoyoneda DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.uliftYoneda Opposite.unop CategoryTheory.ObjectProperty.FullSubcategory.obj EquivLike.toFunLike Opposite.op Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv uliftYonedaCompSheafToPresheaf CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—
uliftYonedaOpCompCoyoneda_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.evaluation CategoryTheory.Functor.whiskeringRight CategoryTheory.uliftFunctor CategoryTheory.Functor.whiskeringLeft CategoryTheory.sheafToPresheaf CategoryTheory.Functor.op uliftYoneda CategoryTheory.coyoneda CategoryTheory.Iso.inv uliftYonedaOpCompCoyoneda DFunLike.coe Equiv CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv	—	—
uliftYonedaOpCompCoyoneda_inv_app_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf CategoryTheory.Functor.comp CategoryTheory.Functor.op yoneda CategoryTheory.sheafCompose CategoryTheory.uliftFunctor CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.evaluation CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft CategoryTheory.coyoneda CategoryTheory.Iso.inv uliftYoneda uliftYonedaOpCompCoyoneda CategoryTheory.uliftYoneda CategoryTheory.uliftYonedaOpCompCoyoneda	—	—
yonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj yoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.id	—	—
yonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj yoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—
yonedaEquiv_naturality 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj yoneda EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.CategoryStruct.comp	—	CategoryTheory.yonedaEquiv_naturality EquivLike.toEmbeddingLike
yonedaEquiv_naturality' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj yoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	yonedaEquiv_naturality
yonedaEquiv_symm_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category yoneda CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv CategoryTheory.Functor.map Opposite.unop Quiver.Hom.op	—	—
yonedaEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Opposite.unop Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category yoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	Equiv.surjective yonedaEquiv_naturality' Equiv.symm_apply_apply
yonedaEquiv_symm_naturality_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj yoneda CategoryTheory.Functor.map DFunLike.coe Equiv CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv Quiver.Hom.op	—	Equiv.injective Equiv.apply_symm_apply yonedaEquiv_yoneda_map
yonedaEquiv_symm_naturality_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj yoneda DFunLike.coe Equiv CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	Equiv.injective Equiv.apply_symm_apply
yonedaEquiv_yoneda_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj yoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.Functor.map	—	yonedaEquiv_apply CategoryTheory.Category.id_comp
yonedaOpCompCoyoneda_hom_app_app_down 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.evaluation CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.op yoneda CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringRight CategoryTheory.uliftFunctor CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.hom yonedaOpCompCoyoneda DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.yoneda Opposite.unop CategoryTheory.ObjectProperty.FullSubcategory.obj EquivLike.toFunLike Opposite.op Equiv.instEquivLike CategoryTheory.yonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv yonedaCompSheafToPresheaf CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—
yonedaOpCompCoyoneda_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.evaluation CategoryTheory.Functor.whiskeringRight CategoryTheory.uliftFunctor CategoryTheory.Functor.whiskeringLeft CategoryTheory.sheafToPresheaf CategoryTheory.Functor.op yoneda CategoryTheory.coyoneda CategoryTheory.Iso.inv yonedaOpCompCoyoneda Opposite.op CategoryTheory.yoneda Opposite.unop CategoryTheory.Iso.hom CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj yonedaCompSheafToPresheaf CategoryTheory.largeCurriedYonedaLemma	—	—
yonedaULiftEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.sheafToPresheaf yoneda CategoryTheory.CategoryStruct.id	—	uliftYonedaEquiv_apply
yonedaULiftEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	uliftYonedaEquiv_comp
yonedaULiftEquiv_naturality 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp	—	uliftYonedaEquiv_naturality
yonedaULiftEquiv_naturality' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.obj uliftYoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	uliftYonedaEquiv_naturality'
yonedaULiftEquiv_symm_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category uliftYoneda CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.sheafToPresheaf yoneda CategoryTheory.Functor.map Opposite.unop Quiver.Hom.op	—	uliftYonedaEquiv_symm_app_apply
yonedaULiftEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op Opposite.unop Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category uliftYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	uliftYonedaEquiv_symm_map
yonedaULiftEquiv_symm_naturality_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.Functor.map DFunLike.coe Equiv CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv Quiver.Hom.op	—	uliftYonedaEquiv_symm_naturality_left
yonedaULiftEquiv_symm_naturality_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda DFunLike.coe Equiv CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	uliftYonedaEquiv_symm_naturality_right
yonedaULiftEquiv_yonedaULift_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.Functor.map CategoryTheory.sheafToPresheaf yoneda	—	uliftYonedaEquiv_uliftYoneda_map

---

← Back to Index