Commit 2026-03-06 00:15 c3371b99

View on Github →

feat(CategoryTheory/Sites): points of presheaf toposes (#35201) Let C be a category. For the Grothendieck topology ⊥, we know that the category of sheaves with values in A identify to Cᵒᵖ ⥤ A. In this PR, we show that any X : C defines a point for this site, and that these points form a conservative family of points.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

added def CategoryTheory.Limits.IsInitial.op

added def CategoryTheory.Limits.IsInitial.unop

added def CategoryTheory.Limits.IsTerminal.op

added def CategoryTheory.Limits.IsTerminal.unop

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

added theorem CategoryTheory.GrothendieckTopology.isConservative_pointsBot

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean