The calculus of fractions deduced from an adjunction #
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.)
theorem
CategoryTheory.Adjunction.hasLeftCalculusOfFractions
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_3, u_1} C₁]
[Category.{u_4, u_2} C₂]
{G : Functor C₁ C₂}
{F : Functor C₂ C₁}
[F.Full]
[F.Faithful]
(adj : G ⊣ F)
:
theorem
CategoryTheory.Adjunction.hasRightCalculusOfFractions
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_4, u_1} C₁]
[Category.{u_3, u_2} C₂]
{G : Functor C₁ C₂}
{F : Functor C₂ C₁}
[F.Full]
[F.Faithful]
(adj : F ⊣ G)
: