Theorem CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology

Modification history

2026-06-05 16:26

Mathlib/CategoryTheory/MorphismProperty/CommaSites.lean

refactor(CategoryTheory/Sites): replace `Functor.inducedTopology` (#39951) …

Modified CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology View on Github →

2026-03-04 16:50

Mathlib/CategoryTheory/MorphismProperty/CommaSites.lean

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

Added CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology View on Github →