Theorem CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf

Modification history

2026-03-16 11:24

Mathlib/CategoryTheory/Sites/Continuous.lean

refactor(CategoryTheory/Sites): remove universe parameter from `Functor.IsContinuous` (#36459) …

Modified CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf View on Github →

2026-03-02 11:18

Mathlib/CategoryTheory/Sites/Continuous.lean

feat(AlgebraicGeometry): constant sheaf associated to a topological space (#35915) …

Added CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf View on Github →