Def CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous

Modification history

2026-04-19 00:33
Mathlib/CategoryTheory/Sites/Pullback.lean
chore: adaptations for overlapping instances linter (#38151) …
Modified CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuousView on Github →
2026-03-16 11:24
Mathlib/CategoryTheory/Sites/Pullback.lean
refactor(CategoryTheory/Sites): remove universe parameter from `Functor.IsContinuous` (#36459) …
Modified CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuousView on Github →
2024-12-19 21:50
Mathlib/CategoryTheory/Sites/Pullback.lean
refactor(CategoryTheory/Sites): define Functor.sheafPullback as a left adjoint (#19516) …
Added CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuousView on Github →