Commit 2025-11-13 16:36 7bf80db9

View on Github →

chore(CategoryTheory/Sites): name change from yonedaULift to uliftYoneda (#31538) Change the name of GrothendieckTopology.yonedaULift to GrothendieckTopology.uliftYoneda to fit the non-sheaf version. Move the definition of GrothendieckTopology.uliftYoneda from the file Subcanonical.lean to the file Canonical.lean, where GrothendieckTopology.yoneda is defined.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

added def CategoryTheory.GrothendieckTopology.uliftYoneda

Modified Mathlib/CategoryTheory/Sites/Subcanonical.lean

added theorem CategoryTheory.GrothendieckTopology.hom_ext_uliftYoneda

deleted theorem CategoryTheory.GrothendieckTopology.hom_ext_yonedaULift

added theorem CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv'

added theorem CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv

deleted theorem CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv'

deleted theorem CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv

added def CategoryTheory.GrothendieckTopology.uliftYonedaEquiv

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality'

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right

added theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULeftEquiv_symm_map

deleted def CategoryTheory.GrothendieckTopology.yonedaULift

deleted def CategoryTheory.GrothendieckTopology.yonedaULiftEquiv

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality'

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right

deleted theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map