Commit 2025-04-28 01:46 efd09be9
View on Github →feat(CategoryTheory/Localization): the calculus of fractions that is deduced from an adjunction (#22748)
If G ⊣ F is an adjunction, and F is fully faithful, then there is a left calculus of fractions for the inverse image by G of the class of isomorphisms.
(The dual statement is also obtained.)