Commit 2026-03-04 16:50 d38b507b

View on Github →

feat(CategoryTheory/MorphismProperty): API for sites on P.Over ⊤ X (#36126) From Proetale

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

added theorem CategoryTheory.MorphismProperty.Over.changeProp_obj_hom

added theorem CategoryTheory.MorphismProperty.Over.changeProp_obj_left

Created Mathlib/CategoryTheory/MorphismProperty/CommaSites.lean

added theorem CategoryTheory.MorphismProperty.exists_map_eq_of_presieve

added theorem CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le

added theorem CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology

Modified Mathlib/CategoryTheory/Sites/DenseSubsite/InducedTopology.lean

added theorem CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem

added theorem CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology

added theorem CategoryTheory.Precoverage.toGrothendieck_comap_le_inducedTopology