Commit 2024-09-05 11:08 ff38cf1a

View on Github →

chore(CategoryTheory/Sites): simplify definition of adjunction between sheaf categories (#16501)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Adjunction.lean

added theorem CategoryTheory.Sheaf.adjunction_counit_app_val

added theorem CategoryTheory.Sheaf.adjunction_unit_app_val

deleted def CategoryTheory.Sheaf.composeEquiv