Documentation Verification Report

Canonical

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

Statistics

Metric	Count
Definitions `fullyFaithfulUliftYoneda`, `uliftYoneda`, `uliftYonedaCompSheafToPresheaf`, `uliftYonedaIsoYoneda`, `yoneda`, `yonedaCompSheafToPresheaf`, `yonedaFullyFaithful`, `yonedaULift`, `canonicalTopology`, `finestTopology`, `finestTopologySingle`	11
Theorems `isSheaf_of_isRepresentable`, `le_canonical`, `of_isSheaf_yoneda_obj`, `of_le`, `instFaithfulSheafTypeUliftYoneda`, `instFaithfulSheafTypeYoneda`, `instFullSheafTypeUliftYoneda`, `instFullSheafTypeYoneda`, `instSubcanonicalCanonicalTopology`, `le_canonical`, `uliftYonedaCompSheafToPresheaf_hom_app_app`, `uliftYonedaCompSheafToPresheaf_inv_app_app`, `uliftYonedaIsoYoneda_hom_app_hom_app`, `uliftYonedaIsoYoneda_inv_app_hom_app_down`, `uliftYoneda_map_hom_app_down`, `uliftYoneda_obj_obj_map_down`, `uliftYoneda_obj_obj_obj`, `yoneda_map_hom`, `yoneda_obj_obj`, `isSheafFor_bind`, `isSheafFor_trans`, `isSheaf_of_isRepresentable`, `isSheaf_yoneda_obj`, `le_finestTopology`, `sheaf_for_finestTopology`	25
Total	36

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`fullyFaithfulUliftYoneda` 📖	CompOp	—
`uliftYoneda` 📖	CompOp	39 math math: `uliftYonedaIsoYoneda_inv_app_hom_app_down`, `yonedaULiftEquiv_apply`, `instFaithfulSheafTypeUliftYoneda`, `uliftYonedaEquiv_naturality`, `uliftYonedaEquiv_naturality'`, `uliftYonedaEquiv_symm_map`, `yonedaULiftEquiv_naturality'`, `instFullSheafTypeUliftYoneda`, `instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf`, `yonedaULiftEquiv_symm_naturality_left`, `yonedaULiftEquiv_symm_naturality_right`, `uliftYonedaEquiv_uliftYoneda_map`, `uliftYonedaCompSheafToPresheaf_inv_app_app`, `uliftYonedaCompSheafToPresheaf_hom_app_app`, `uliftYonedaEquiv_symm_app_apply`, `uliftYoneda_obj_obj_map_down`, `uliftYoneda_obj_obj_obj`, `uliftYonedaIsoYoneda_hom_app_hom_app`, `map_uliftYonedaEquiv'`, `map_yonedaULiftEquiv'`, `uliftYonedaEquiv_apply`, `uliftYonedaOpCompCoyoneda_hom_app_app_down`, `uliftYonedaEquiv_symm_naturality_left`, `instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf`, `instPreservesLimitsOfShapeSheafTypeUliftYoneda`, `uliftYonedaOpCompCoyoneda_app_app`, `yonedaULiftEquiv_naturality`, `map_uliftYonedaEquiv`, `uliftYonedaOpCompCoyoneda_inv_app_app`, `yonedaULiftEquiv_comp`, `yonedaULiftEquiv_symm_app_apply`, `yonedaULiftEquiv_symm_map`, `uliftYonedaEquiv_symm_naturality_right`, `uliftYoneda_map_hom_app_down`, `yonedaULiftEquiv_yonedaULift_map`, `map_yonedaULiftEquiv`, `uliftYonedaOpCompCoyoneda_inv_app_app_hom_app`, `instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf`, `uliftYonedaEquiv_comp`
`uliftYonedaCompSheafToPresheaf` 📖	CompOp	3 math math: `uliftYonedaCompSheafToPresheaf_inv_app_app`, `uliftYonedaCompSheafToPresheaf_hom_app_app`, `uliftYonedaOpCompCoyoneda_hom_app_app_down`
`uliftYonedaIsoYoneda` 📖	CompOp	2 math math: `uliftYonedaIsoYoneda_inv_app_hom_app_down`, `uliftYonedaIsoYoneda_hom_app_hom_app`
`yoneda` 📖	CompOp	49 math math: `preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem`, `yonedaOpCompCoyoneda_hom_app_app_down`, `LightCondensed.ihomPoints_apply`, `uliftYonedaIsoYoneda_inv_app_hom_app_down`, `yonedaULiftEquiv_apply`, `yonedaEquiv_symm_app_apply`, `AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType`, `instFullSheafTypeYoneda`, `yonedaEquiv_naturality'`, `uliftYonedaEquiv_uliftYoneda_map`, `yonedaOpCompCoyoneda_inv_app_app`, `map_yonedaEquiv'`, `yonedaEquiv_comp`, `yonedaEquiv_symm_map`, `uliftYonedaEquiv_symm_app_apply`, `AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc`, `uliftYoneda_obj_obj_map_down`, `instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf`, `instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf`, `uliftYonedaIsoYoneda_hom_app_hom_app`, `AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf`, `preservesLimitsOfSize_yoneda`, `map_uliftYonedaEquiv'`, `AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf`, `yonedaEquiv_naturality`, `AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf`, `map_yonedaULiftEquiv'`, `uliftYonedaEquiv_apply`, `instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1`, `uliftYonedaOpCompCoyoneda_hom_app_app_down`, `LightCondensed.ihomPoints_symm_apply`, `instFaithfulSheafTypeYoneda`, `map_uliftYonedaEquiv`, `AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp`, `instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf`, `yonedaULiftEquiv_symm_app_apply`, `yonedaEquiv_symm_naturality_left`, `yoneda_map_hom`, `yoneda_obj_obj`, `map_yonedaEquiv`, `uliftYoneda_map_hom_app_down`, `yonedaULiftEquiv_yonedaULift_map`, `map_yonedaULiftEquiv`, `uliftYonedaOpCompCoyoneda_inv_app_app_hom_app`, `AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued`, `instPreservesLimitsOfShapeSheafTypeYoneda`, `yonedaEquiv_yoneda_map`, `yonedaEquiv_apply`, `yonedaEquiv_symm_naturality_right`
`yonedaCompSheafToPresheaf` 📖	CompOp	2 math math: `yonedaOpCompCoyoneda_hom_app_app_down`, `yonedaOpCompCoyoneda_inv_app_app`
`yonedaFullyFaithful` 📖	CompOp	—
`yonedaULift` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulSheafTypeUliftYoneda` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `uliftYoneda`	—	`CategoryTheory.Functor.FullyFaithful.faithful`
`instFaithfulSheafTypeYoneda` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `yoneda`	—	`CategoryTheory.Functor.FullyFaithful.faithful`
`instFullSheafTypeUliftYoneda` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `uliftYoneda`	—	`CategoryTheory.Functor.FullyFaithful.full`
`instFullSheafTypeYoneda` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `yoneda`	—	`CategoryTheory.Functor.FullyFaithful.full`
`instSubcanonicalCanonicalTopology` 📖	mathematical	—	`Subcanonical` `CategoryTheory.Sheaf.canonicalTopology`	—	`le_rfl`
`le_canonical` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology` `instLEGrothendieckTopology` `CategoryTheory.Sheaf.canonicalTopology`	—	`Subcanonical.le_canonical`
`uliftYonedaCompSheafToPresheaf_hom_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Presheaf.IsSheaf` `uliftYoneda` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Iso.hom` `CategoryTheory.uliftYoneda` `uliftYonedaCompSheafToPresheaf`	—	—
`uliftYonedaCompSheafToPresheaf_inv_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Presheaf.IsSheaf` `uliftYoneda` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Iso.inv` `CategoryTheory.uliftYoneda` `uliftYonedaCompSheafToPresheaf`	—	—
`uliftYonedaIsoYoneda_hom_app_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafToPresheaf` `uliftYoneda` `yoneda` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Iso.hom` `uliftYonedaIsoYoneda` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	—
`uliftYonedaIsoYoneda_inv_app_hom_app_down` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafToPresheaf` `yoneda` `CategoryTheory.NatTrans.app` `uliftYoneda` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Iso.inv` `uliftYonedaIsoYoneda`	—	—
`uliftYoneda_map_hom_app_down` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafToPresheaf` `yoneda` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.uliftFunctor` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.sheafCompose` `CategoryTheory.Functor.map` `uliftYoneda` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver`	—	—
`uliftYoneda_obj_obj_map_down` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafToPresheaf` `yoneda` `CategoryTheory.Functor.map` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `uliftYoneda` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `Quiver.Hom`	—	—
`uliftYoneda_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `uliftYoneda` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	—
`yoneda_map_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.yoneda` `CategoryTheory.Functor.map` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `yoneda`	—	—
`yoneda_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `yoneda` `CategoryTheory.yoneda`	—	—

CategoryTheory.GrothendieckTopology.Subcanonical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheaf_of_isRepresentable` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheaf`	—	`CategoryTheory.Presieve.isSheaf_of_le` `CategoryTheory.GrothendieckTopology.le_canonical` `CategoryTheory.Sheaf.isSheaf_of_isRepresentable`
`le_canonical` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `CategoryTheory.Sheaf.canonicalTopology`	—	—
`of_isSheaf_yoneda_obj` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda`	`CategoryTheory.GrothendieckTopology.Subcanonical`	—	`CategoryTheory.Sheaf.le_finestTopology`
`of_le` 📖	mathematical	`CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology`	`CategoryTheory.GrothendieckTopology.Subcanonical`	—	`of_isSheaf_yoneda_obj` `CategoryTheory.Presieve.IsSheaf.isSheafFor` `isSheaf_of_isRepresentable` `CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda` `CategoryTheory.Sieve.generate_sieve`

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`canonicalTopology` 📖	CompOp	6 math math: `CategoryTheory.typesGrothendieckTopology_eq_canonical`, `CategoryTheory.GrothendieckTopology.instSubcanonicalCanonicalTopology`, `CategoryTheory.GrothendieckTopology.Subcanonical.le_canonical`, `isSheaf_of_isRepresentable`, `isSheaf_yoneda_obj`, `CategoryTheory.GrothendieckTopology.le_canonical`
`finestTopology` 📖	CompOp	2 math math: `sheaf_for_finestTopology`, `le_finestTopology`
`finestTopologySingle` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheafFor_bind` 📖	mathematical	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Sieve.arrows` `CategoryTheory.Presieve.IsSeparatedFor` `CategoryTheory.Sieve.pullback`	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.bind`	—	`CategoryTheory.Presieve.isSheafFor_bind`
`isSheafFor_trans` 📖	mathematical	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Sieve.arrows` `CategoryTheory.Presieve.IsSeparatedFor` `CategoryTheory.Sieve.pullback`	`CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Sieve.arrows`	—	`CategoryTheory.Presieve.isSheafFor_trans`
`isSheaf_of_isRepresentable` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheaf` `canonicalTopology`	—	`CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff` `CategoryTheory.Presieve.isSheaf_iso` `CategoryTheory.Functor.instIsRepresentableCompOppositeUliftFunctor` `CategoryTheory.isSheaf_iff_isSheaf_of_type` `CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor` `isSheaf_yoneda_obj`
`isSheaf_yoneda_obj` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheaf` `canonicalTopology` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.yoneda`	—	`sheaf_for_finestTopology` `Set.mem_range_self`
`le_finestTopology` 📖	mathematical	`CategoryTheory.Presieve.IsSheaf`	`CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `finestTopology`	—	`CategoryTheory.GrothendieckTopology.pullback_stable`
`sheaf_for_finestTopology` 📖	mathematical	`CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Set` `Set.instMembership`	`CategoryTheory.Presieve.IsSheaf` `finestTopology`	—	`CategoryTheory.Sieve.pullback_id`

---

← Back to Index