Commit 2025-12-11 00:39 c56c733d

View on Github →

feat(CategoryTheory/Sites): the category structure on the points of a site (#31711)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Sites/Point/Basic.lean

added theorem CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext

added theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc

Created Mathlib/CategoryTheory/Sites/Point/Category.lean

added theorem CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp

added theorem CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_id

added theorem CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp

added theorem CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_id

added structure CategoryTheory.GrothendieckTopology.Point.Hom

added theorem CategoryTheory.GrothendieckTopology.Point.comp_hom

added theorem CategoryTheory.GrothendieckTopology.Point.hom_ext

added theorem CategoryTheory.GrothendieckTopology.Point.id_hom

Modified docs/references.bib