Lifting of bifunctors

In this file, in the context of the localization of categories, we extend the notion of lifting of functors to the case of bifunctors. As the localization of categories behaves well with respect to finite products of categories (when the classes of morphisms contain identities), all the definitions for bifunctors C₁ ⥤ C₂ ⥤ E are obtained by reducing to the case of functors (C₁ × C₂) ⥤ E by using currying and uncurrying.

Given morphism properties W₁ : MorphismProperty C₁ and W₂ : MorphismProperty C₂, and a functor F : C₁ ⥤ C₂ ⥤ E, we define MorphismProperty.IsInvertedBy₂ W₁ W₂ F as the condition that the functor uncurry.obj F : C₁ × C₂ ⥤ E inverts W₁.prod W₂.

If L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ are localization functors for W₁ and W₂ respectively, and F : C₁ ⥤ C₂ ⥤ E satisfies MorphismProperty.IsInvertedBy₂ W₁ W₂ F, we introduce Localization.lift₂ F hF L₁ L₂ : D₁ ⥤ D₂ ⥤ E which is a bifunctor which lifts F.

def CategoryTheory.MorphismProperty.IsInvertedBy₂ {C₁ : Type u_1} {C₂ : Type u_2} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_5} E] (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (F : Functor C₁ (Functor C₂ E)) : Prop

Classes of morphisms W₁ : MorphismProperty C₁ and W₂ : MorphismProperty C₂ are said to be inverted by F : C₁ ⥤ C₂ ⥤ E if W₁.prod W₂ is inverted by the functor uncurry.obj F : C₁ × C₂ ⥤ E.

class CategoryTheory.Localization.Lifting₂ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (F : Functor C₁ (Functor C₂ E)) (F' : Functor D₁ (Functor D₂ E)) : Type (max (max u_1 u_11) u_2)

Given functors L₁ : C₁ ⥤ D₁, L₂ : C₂ ⥤ D₂, morphisms properties W₁ on C₁ and W₂ on C₂, and functors F : C₁ ⥤ C₂ ⥤ E and F' : D₁ ⥤ D₂ ⥤ E, we say Lifting₂ L₁ L₂ W₁ W₂ F F' holds if F is induced by F', up to an isomorphism.

• iso' : (((Functor.whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F

  the isomorphism (((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F expressing that F is induced by F' up to an isomorphism

noncomputable def CategoryTheory.Localization.Lifting₂.iso {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (F : Functor C₁ (Functor C₂ E)) (F' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F F'] : (((Functor.whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F

The isomorphism (((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F when Lifting₂ L₁ L₂ W₁ W₂ F F' holds.

noncomputable def CategoryTheory.Localization.Lifting₂.fst {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (F : Functor C₁ (Functor C₂ E)) (F' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F F'] (X₁ : C₁) : Lifting L₂ W₂ (F.obj X₁) (F'.obj (L₁.obj X₁))

If Lifting₂ L₁ L₂ W₁ W₂ F F' holds, then Lifting L₂ W₂ (F.obj X₁) (F'.obj (L₁.obj X₁)) holds for any X₁ : C₁.

noncomputable instance CategoryTheory.Localization.Lifting₂.flip {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (F : Functor C₁ (Functor C₂ E)) (F' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F F'] : Lifting₂ L₂ L₁ W₂ W₁ F.flip F'.flip

noncomputable def CategoryTheory.Localization.Lifting₂.snd {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (F : Functor C₁ (Functor C₂ E)) (F' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F F'] (X₂ : C₂) : Lifting L₁ W₁ (F.flip.obj X₂) (F'.flip.obj (L₂.obj X₂))

If Lifting₂ L₁ L₂ W₁ W₂ F F' holds, then Lifting L₁ W₁ (F.flip.obj X₂) (F'.flip.obj (L₂.obj X₂)) holds for any X₂ : C₂.

noncomputable instance CategoryTheory.Localization.Lifting₂.uncurry {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (F : Functor C₁ (Functor C₂ E)) (F' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F F'] : Lifting (L₁.prod L₂) (W₁.prod W₂) (Functor.uncurry.obj F) (Functor.uncurry.obj F')

noncomputable def CategoryTheory.Localization.lift₂ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (F : Functor C₁ (Functor C₂ E)) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] : Functor D₁ (Functor D₂ E)

Given localization functor L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ with respect to W₁ : MorphismProperty C₁ and W₂ : MorphismProperty C₂ respectively, and a bifunctor F : C₁ ⥤ C₂ ⥤ E which inverts W₁ and W₂, this is the induced localized bifunctor D₁ ⥤ D₂ ⥤ E.

noncomputable instance CategoryTheory.Localization.instLifting₂Lift₂ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (F : Functor C₁ (Functor C₂ E)) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] : Lifting₂ L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂)

noncomputable instance CategoryTheory.Localization.Lifting₂.liftingLift₂ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (F : Functor C₁ (Functor C₂ E)) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] (X₁ : C₁) : Lifting L₂ W₂ (F.obj X₁) ((lift₂ F hF L₁ L₂).obj (L₁.obj X₁))

noncomputable instance CategoryTheory.Localization.Lifting₂.liftingLift₂Flip {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (F : Functor C₁ (Functor C₂ E)) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] (X₂ : C₂) : Lifting L₁ W₁ (F.flip.obj X₂) ((lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂))

theorem CategoryTheory.Localization.lift₂_iso_hom_app_app₁ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_9, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_10, u_3} D₁] [Category.{u_11, u_4} D₂] [Category.{u_7, u_5} E] (F : Functor C₁ (Functor C₂ E)) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] (X₁ : C₁) (X₂ : C₂) : ((Lifting₂.iso L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂)).hom.app X₁).app X₂ = (Lifting.iso L₂ W₂ (F.obj X₁) ((lift₂ F hF L₁ L₂).obj (L₁.obj X₁))).hom.app X₂

theorem CategoryTheory.Localization.lift₂_iso_hom_app_app₂ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_9, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_10, u_3} D₁] [Category.{u_11, u_4} D₂] [Category.{u_7, u_5} E] (F : Functor C₁ (Functor C₂ E)) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] (X₁ : C₁) (X₂ : C₂) : ((Lifting₂.iso L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂)).hom.app X₁).app X₂ = (Lifting.iso L₁ W₁ (F.flip.obj X₂) ((lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂))).hom.app X₁

noncomputable def CategoryTheory.Localization.lift₂NatTrans {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ E)) (F₁' F₂' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'] [Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (τ : F₁ ⟶ F₂) : F₁' ⟶ F₂'

The natural transformation F₁' ⟶ F₂' of bifunctors induced by a natural transformation τ : F₁ ⟶ F₂ when Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁' and Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂' hold.

@[simp]

theorem CategoryTheory.Localization.lift₂NatTrans_app_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_8, u_1} C₁] [Category.{u_9, u_2} C₂] [Category.{u_11, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_7, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ E)) (F₁' F₂' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'] [Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) : ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) = CategoryStruct.comp (((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂) (CategoryStruct.comp ((τ.app X₁).app X₂) (((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂))

theorem CategoryTheory.Localization.natTrans₂_ext {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_8, u_3} D₁] [Category.{u_9, u_4} D₂] [Category.{u_7, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] {F₁' F₂' : Functor D₁ (Functor D₂ E)} {τ τ' : F₁' ⟶ F₂'} (h : ∀ (X₁ : C₁) (X₂ : C₂), (τ.app (L₁.obj X₁)).app (L₂.obj X₂) = (τ'.app (L₁.obj X₁)).app (L₂.obj X₂)) : τ = τ'

noncomputable def CategoryTheory.Localization.lift₂NatIso {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} D₁] [Category.{u_10, u_4} D₂] [Category.{u_11, u_5} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [W₁.ContainsIdentities] [W₂.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ E)) (F₁' F₂' : Functor D₁ (Functor D₂ E)) [Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'] [Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (e : F₁ ≅ F₂) : F₁' ≅ F₂'

The natural isomorphism F₁' ≅ F₂' of bifunctors induced by a natural isomorphism e : F₁ ≅ F₂ when Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁' and Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂' hold.