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, 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_val_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	44
Total	51

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
Subcanonical 📖	CompData	8 math math: CategoryTheory.regularTopology.subcanonical, CategoryTheory.extensiveTopology.subcanonical, CategoryTheory.coherentTopology.subcanonical, instSubcanonicalCanonicalTopology, Subcanonical.of_isSheaf_yoneda_obj, CategoryTheory.subcanonical_typesGrothendieckTopology, 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_val_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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda	—	—	CategoryTheory.Sheaf.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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda	—	—	CategoryTheory.Sheaf.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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda	—	—	hom_ext_uliftYoneda
map_uliftYonedaEquiv 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val yoneda	—	uliftYonedaEquiv_naturality uliftYonedaEquiv_comp uliftYonedaEquiv_uliftYoneda_map
map_uliftYonedaEquiv' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val yoneda Quiver.Hom.unop	—	uliftYonedaEquiv_naturality' uliftYonedaEquiv_comp uliftYonedaEquiv_uliftYoneda_map
map_yonedaEquiv 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	yonedaEquiv_naturality yonedaEquiv_comp yonedaEquiv_yoneda_map
map_yonedaEquiv' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val Quiver.Hom.unop	—	yonedaEquiv_naturality' yonedaEquiv_comp yonedaEquiv_yoneda_map
map_yonedaULiftEquiv 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val yoneda	—	map_uliftYonedaEquiv
map_yonedaULiftEquiv' 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val 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.Sheaf.instCategorySheaf 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.Sheaf.instCategorySheaf yoneda	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.yonedaFunctor_preservesLimits CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf
uliftYonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val yoneda CategoryTheory.CategoryStruct.id	—	—
uliftYonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	—
uliftYonedaEquiv_naturality 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf uliftYoneda CategoryTheory.Sheaf.Hom.val DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv 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.Sheaf.val Opposite.op Opposite.unop Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.Functor.map DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val 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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.Functor.map yoneda	—	uliftYonedaEquiv_apply CategoryTheory.Category.id_comp
uliftYonedaOpCompCoyoneda_app_app 📖	mathematical	—	CategoryTheory.Iso.app CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category 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.Sheaf.val 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.Sheaf.instCategorySheaf 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.Sheaf.val EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv uliftYonedaCompSheafToPresheaf CategoryTheory.Sheaf.Hom.val	—	—
uliftYonedaOpCompCoyoneda_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category 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.Sheaf.val Opposite.op Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv	—	—
uliftYonedaOpCompCoyoneda_inv_app_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.category CategoryTheory.sheafToPresheaf CategoryTheory.Functor.comp CategoryTheory.Functor.op yoneda CategoryTheory.sheafCompose CategoryTheory.uliftFunctor CategoryTheory.Sheaf.Hom.val CategoryTheory.evaluation CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft CategoryTheory.coyoneda CategoryTheory.Iso.inv uliftYoneda uliftYonedaOpCompCoyoneda CategoryTheory.uliftYoneda CategoryTheory.Sheaf.val CategoryTheory.uliftYonedaOpCompCoyoneda	—	—
yonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val CategoryTheory.CategoryStruct.id	—	—
yonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	—
yonedaEquiv_naturality 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf yoneda CategoryTheory.Sheaf.Hom.val 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.Sheaf.val Opposite.op Opposite.unop Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda CategoryTheory.Functor.map DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val 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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj yoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val 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.Sheaf.instCategorySheaf 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.Sheaf.val EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.yonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv yonedaCompSheafToPresheaf CategoryTheory.Sheaf.Hom.val	—	—
yonedaOpCompCoyoneda_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category 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.Sheaf.val yonedaCompSheafToPresheaf CategoryTheory.largeCurriedYonedaLemma	—	—
yonedaULiftEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val 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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	uliftYonedaEquiv_comp
yonedaULiftEquiv_naturality 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf uliftYoneda CategoryTheory.Sheaf.Hom.val DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv 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.Sheaf.val Opposite.op Opposite.unop Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda CategoryTheory.Functor.map DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val 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.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	uliftYonedaEquiv_symm_naturality_right
yonedaULiftEquiv_yonedaULift_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj uliftYoneda Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryTheory.Functor.map yoneda	—	uliftYonedaEquiv_uliftYoneda_map

---

← Back to Index