The calculus of fractions deduced from an adjunction #
If G ⊣ F is an adjunction, F is fully faithful,
and W is a class of morphisms that is inverted by G
and such that the morphism adj.unit.app X belongs to W
for any object X, then G is a localization functor
with respect to W. Moreover, if W is multiplicative,
then W has a calculus of left fractions. This
holds in particular if W is the inverse image of
the class of isomorphisms by G.
(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₁}
(adj : G ⊣ F)
(W : MorphismProperty C₁)
[W.IsMultiplicative]
(hW : W.IsInvertedBy G)
(hW' : W.functorCategory C₁ adj.unit)
:
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₁}
(adj : F ⊣ G)
(W : MorphismProperty C₁)
[W.IsMultiplicative]
(hW : W.IsInvertedBy G)
(hW' : W.functorCategory C₁ adj.counit)
:
theorem
CategoryTheory.Adjunction.isLocalization_leftAdjoint
{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)
(W : MorphismProperty C₁)
(hW : W.IsInvertedBy G)
(hW' : W.functorCategory C₁ adj.unit)
:
G.IsLocalization W
theorem
CategoryTheory.Adjunction.isLocalization_rightAdjoint
{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)
(W : MorphismProperty C₁)
(hW : W.IsInvertedBy G)
(hW' : W.functorCategory C₁ adj.counit)
:
G.IsLocalization W
theorem
CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_unit
{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)
:
((MorphismProperty.isomorphisms C₂).inverseImage G).functorCategory C₁ adj.unit
theorem
CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_counit
{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)
:
((MorphismProperty.isomorphisms C₂).inverseImage G).functorCategory C₁ adj.counit
theorem
CategoryTheory.Adjunction.isLocalization_leftAdjoint'
{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.isLocalization_rightAdjoint'
{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)
:
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)
: