Theorem CategoryTheory.Sheaf.adjunction_counit_app_val

Modification history

2026-03-06 08:34
Mathlib/CategoryTheory/Sites/Adjunction.lean
refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` (#36081) …
Deleted CategoryTheory.Sheaf.adjunction_counit_app_valView on Github →
2024-09-05 11:08
Mathlib/CategoryTheory/Sites/Adjunction.lean
chore(CategoryTheory/Sites): simplify definition of adjunction between sheaf categories (#16501)
Added CategoryTheory.Sheaf.adjunction_counit_app_valView on Github →