Commit 2026-05-28 21:17 7c06f324

View on Github →

feat(CategoryTheory/Sites): continuous functors preserve covers (#39961) We also add some pre-requisites needed for #39951.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Continuous.lean

added theorem CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf_type

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

added theorem CategoryTheory.Functor.IsCocontinuous.iff_of_iso

added theorem CategoryTheory.Functor.IsCocontinuous.of_iso

Modified Mathlib/CategoryTheory/Sites/CoverPreserving.lean

added theorem CategoryTheory.CoverPreserving.of_isContinuous

added theorem CategoryTheory.Functor.isContinuous_iff_coverPreserving

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

added theorem CategoryTheory.Precoverage.comap_monotone

Modified Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.map_bot