Commit 2024-11-01 22:15 c89d8462

View on Github →

feat(CategoryTheory/Sites): some API for the Yoneda embedding into sheaf categories (#18185)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

Created Mathlib/CategoryTheory/Sites/Subcanonical.lean

added theorem CategoryTheory.GrothendieckTopology.hom_ext_yoneda

added theorem CategoryTheory.GrothendieckTopology.hom_ext_yonedaULift

added theorem CategoryTheory.GrothendieckTopology.map_yonedaEquiv'

added theorem CategoryTheory.GrothendieckTopology.map_yonedaEquiv

added theorem CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv'

added theorem CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv

added def CategoryTheory.GrothendieckTopology.yonedaEquiv

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_apply

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_comp

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality'

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right

added theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map

added theorem CategoryTheory.GrothendieckTopology.yonedaULeftEquiv_symm_map

added def CategoryTheory.GrothendieckTopology.yonedaULift

added def CategoryTheory.GrothendieckTopology.yonedaULiftEquiv

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality'

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right

added theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.yonedaEquiv_symm_naturality_left

added theorem CategoryTheory.yonedaEquiv_symm_naturality_right