Commit 2024-04-26 15:11 38faa1d2

View on Github →

chore(CategoryTheory/Adjunction): move Adjunction.restrictFullyFaithful to separate file (#12363) Also resolves a TODO to add lemmas about Adjunction.restrictFullyFaithful

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

deleted def CategoryTheory.Adjunction.restrictFullyFaithful

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

Created Mathlib/CategoryTheory/Adjunction/Restrict.lean

added theorem CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app

added theorem CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app

added def CategoryTheory.Adjunction.restrictFullyFaithful

Modified Mathlib/CategoryTheory/Sites/Pullback.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean