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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, 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.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} [F.Full] [F.Faithful] (adj : F ⊣ G) :