feat(CategoryTheory/Localization): liftings of bifunctors (#19894)

When a functor `F : C ⥤ E` inverts a class of morphisms `W : MorphismProperty C` and `L : C ⥤ D` is a localization functor for `W`, then `F` lifts as a functor `D ⥤ E`. In this PR, this is generalized to bifunctors (or "functors in two variables") `F : C₁ ⥤ C₂ ⥤ E`, which may be lifted as a functor `D₁ ⥤ D₂ ⥤ E` under similar assumptions.

(We shall also need a version of this in three variables.)

Mathlib.lean

@@ -1923,6 +1923,7 @@ import Mathlib.CategoryTheory.Linear.FunctorCategory
 import Mathlib.CategoryTheory.Linear.LinearFunctor
 import Mathlib.CategoryTheory.Linear.Yoneda
 import Mathlib.CategoryTheory.Localization.Adjunction
+import Mathlib.CategoryTheory.Localization.Bifunctor
 import Mathlib.CategoryTheory.Localization.Bousfield
 import Mathlib.CategoryTheory.Localization.CalculusOfFractions
 import Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows

Mathlib/CategoryTheory/Functor/Category.lean

@@ -142,6 +142,18 @@ protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where
 
 end Functor
 
+variable (C D E) in
+/-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/
+@[simps]
+def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where
+  obj F := F.flip
+  map {F₁ F₂} φ :=
+    { app := fun Y =>
+        { app := fun X => (φ.app X).app Y
+          naturality := fun X₁ X₂ f => by
+            dsimp
+            simp only [← NatTrans.comp_app, naturality] } }
+
 namespace Iso
 
 @[reassoc (attr := simp)]

Mathlib/CategoryTheory/Functor/Currying.lean

@@ -88,6 +88,26 @@ def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E where
       dsimp at f₁ f₂ ⊢
       simp only [← F.map_comp, prod_comp, Category.comp_id, Category.id_comp]))
 
+/-- The functor `uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E` is fully faithful. -/
+def fullyFaithfulUncurry : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).FullyFaithful :=
+  currying.fullyFaithfulFunctor
+
+instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Full :=
+  fullyFaithfulUncurry.full
+
+instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Faithful :=
+  fullyFaithfulUncurry.faithful
+
+/-- Given functors `F₁ : C ⥤ D`, `F₂ : C' ⥤ D'` and `G : D × D' ⥤ E`, this is the isomorphism
+between `curry.obj ((F₁.prod F₂).comp G)` and
+`F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂` in the category `C ⥤ C' ⥤ E`. -/
+@[simps!]
+def curryObjProdComp {C' D' : Type*} [Category C'] [Category D']
+    (F₁ : C ⥤ D) (F₂ : C' ⥤ D') (G : D × D' ⥤ E) :
+    curry.obj ((F₁.prod F₂).comp G) ≅
+      F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂ :=
+  NatIso.ofComponents (fun X₁ ↦ NatIso.ofComponents (fun X₂ ↦ Iso.refl _))
+
 /-- `F.flip` is isomorphic to uncurrying `F`, swapping the variables, and currying. -/
 @[simps!]
 def flipIsoCurrySwapUncurry (F : C ⥤ D ⥤ E) : F.flip ≅ curry.obj (Prod.swap _ _ ⋙ uncurry.obj F) :=

Mathlib/CategoryTheory/Localization/Bifunctor.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2023 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Localization.Prod
+import Mathlib.CategoryTheory.Functor.Currying
+
+/-!
+# 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`.
+
+-/
+
+namespace CategoryTheory
+
+open Category
+
+variable {C₁ C₂ D₁ D₂ E E' : Type*} [Category C₁] [Category C₂]
+  [Category D₁] [Category D₂] [Category E] [Category E']
+
+namespace MorphismProperty
+
+/-- 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`. -/
+def IsInvertedBy₂ (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂)
+    (F : C₁ ⥤ C₂ ⥤ E) : Prop :=
+  (W₁.prod W₂).IsInvertedBy (uncurry.obj F)
+
+end MorphismProperty
+
+namespace Localization
+
+section
+
+variable (L₁ : C₁ ⥤ D₁) (L₂ : C₂ ⥤ D₂)
+
+/-- 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. -/
+class Lifting₂ (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂)
+    (F : C₁ ⥤ C₂ ⥤ E) (F' : D₁ ⥤ D₂ ⥤ E) where
+  /-- the isomorphism `(((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F` expressing
+  that `F` is induced by `F'` up to an isomorphism -/
+  iso' : (((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F
+
+variable (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂)
+  (F : C₁ ⥤ C₂ ⥤ E) (F' : D₁ ⥤ D₂ ⥤ E) [Lifting₂ L₁ L₂ W₁ W₂ F F']
+
+/-- The isomorphism `(((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F` when
+`Lifting₂ L₁ L₂ W₁ W₂ F F'` holds. -/
+noncomputable def Lifting₂.iso : (((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F :=
+  Lifting₂.iso' W₁ W₂
+
+/-- 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 def Lifting₂.fst (X₁ : C₁) :
+    Lifting L₂ W₂ (F.obj X₁) (F'.obj (L₁.obj X₁)) where
+  iso' := ((evaluation _ _).obj X₁).mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ F F')
+
+noncomputable instance Lifting₂.flip : Lifting₂ L₂ L₁ W₂ W₁ F.flip F'.flip where
+  iso' := (flipFunctor _ _ _).mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ F F')
+
+/-- 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 def Lifting₂.snd (X₂ : C₂) :
+    Lifting L₁ W₁ (F.flip.obj X₂) (F'.flip.obj (L₂.obj X₂)) :=
+  Lifting₂.fst L₂ L₁ W₂ W₁ F.flip F'.flip X₂
+
+noncomputable instance Lifting₂.uncurry [Lifting₂ L₁ L₂ W₁ W₂ F F'] :
+    Lifting (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F) (uncurry.obj F') where
+  iso' := CategoryTheory.uncurry.mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ F F')
+
+end
+
+section
+
+variable (F : C₁ ⥤ C₂ ⥤ E) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂}
+  (hF : MorphismProperty.IsInvertedBy₂ W₁ W₂ F)
+  (L₁ : C₁ ⥤ D₁) (L₂ : C₂ ⥤ D₂)
+  [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
+  [W₁.ContainsIdentities] [W₂.ContainsIdentities]
+
+/-- 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 def lift₂ : D₁ ⥤ D₂ ⥤ E :=
+  curry.obj (lift (uncurry.obj F) hF (L₁.prod L₂))
+
+noncomputable instance : Lifting₂ L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂) where
+  iso' := (curryObjProdComp _ _ _).symm ≪≫
+    curry.mapIso (fac (uncurry.obj F) hF (L₁.prod L₂)) ≪≫
+    currying.unitIso.symm.app F
+
+noncomputable instance Lifting₂.liftingLift₂ (X₁ : C₁) :
+    Lifting L₂ W₂ (F.obj X₁) ((lift₂ F hF L₁ L₂).obj (L₁.obj X₁)) :=
+  Lifting₂.fst _ _ W₁ _ _ _ _
+
+noncomputable instance Lifting₂.liftingLift₂Flip (X₂ : C₂) :
+    Lifting L₁ W₁ (F.flip.obj X₂) ((lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂)) :=
+  Lifting₂.snd _ _ _ W₂ _ _ _
+
+lemma lift₂_iso_hom_app_app₁ (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₂ :=
+  rfl
+
+lemma lift₂_iso_hom_app_app₂ (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₁ :=
+  rfl
+
+end
+
+section
+
+variable (L₁ : C₁ ⥤ D₁) (L₂ : C₂ ⥤ D₂)
+  (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂)
+  [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
+  [W₁.ContainsIdentities] [W₂.ContainsIdentities]
+  (F₁ F₂ : C₁ ⥤ C₂ ⥤ E) (F₁' F₂' : D₁ ⥤ D₂ ⥤ E)
+  [Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'] [Lifting₂ L₁ L₂ W₁ W₂ 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. -/
+noncomputable def lift₂NatTrans (τ : F₁ ⟶ F₂) : F₁' ⟶ F₂' :=
+  fullyFaithfulUncurry.preimage
+    (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F₁)
+      (uncurry.obj F₂) (uncurry.obj F₁') (uncurry.obj F₂') (uncurry.map τ))
+
+@[simp]
+theorem lift₂NatTrans_app_app (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) :
+    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) =
+      ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫ (τ.app X₁).app X₂ ≫
+        ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂ := by
+  dsimp [lift₂NatTrans, fullyFaithfulUncurry, Equivalence.fullyFaithfulFunctor]
+  simp only [currying_unitIso_hom_app_app_app, currying_unitIso_inv_app_app_app, comp_id, id_comp]
+  exact liftNatTrans_app _ _ _ _ (uncurry.obj F₁') (uncurry.obj F₂') (uncurry.map τ) ⟨X₁, X₂⟩
+
+variable {F₁' F₂'} in
+include W₁ W₂ in
+theorem natTrans₂_ext {τ τ' : F₁' ⟶ F₂'}
+    (h : ∀ (X₁ : C₁) (X₂ : C₂), (τ.app (L₁.obj X₁)).app (L₂.obj X₂) =
+      (τ'.app (L₁.obj X₁)).app (L₂.obj X₂)) : τ = τ' :=
+  uncurry.map_injective (natTrans_ext (L₁.prod L₂) (W₁.prod W₂) (fun _ ↦ h _ _))
+
+/-- 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. -/
+noncomputable def lift₂NatIso (e : F₁ ≅ F₂) : F₁' ≅ F₂' where
+  hom := lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom
+  inv := lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv
+  hom_inv_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by aesop_cat)
+  inv_hom_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by aesop_cat)
+
+end
+
+end Localization
+
+end CategoryTheory

Mathlib/CategoryTheory/Localization/Predicate.lean

@@ -266,7 +266,7 @@ lemma faithful_whiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*)
 
 variable {E}
 
-theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} (τ τ' : F₁ ⟶ F₂)
+theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} {τ τ' : F₁ ⟶ F₂}
     (h : ∀ X : C, τ.app (L.obj X) = τ'.app (L.obj X)) : τ = τ' := by
   haveI := essSurj L W
   ext Y
@@ -331,13 +331,13 @@ theorem comp_liftNatTrans (F₁ F₂ F₃ : C ⥤ E) (F₁' F₂' F₃' : D ⥤
     [h₂ : Lifting L W F₂ F₂'] [h₃ : Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) :
     liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ' =
       liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ') :=
-  natTrans_ext L W _ _ fun X => by
+  natTrans_ext L W fun X => by
     simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]
 
 @[simp]
 theorem liftNatTrans_id (F : C ⥤ E) (F' : D ⥤ E) [h : Lifting L W F F'] :
     liftNatTrans L W F F F' F' (𝟙 F) = 𝟙 F' :=
-  natTrans_ext L W _ _ fun X => by
+  natTrans_ext L W fun X => by
     simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]
     rfl
 

Mathlib/CategoryTheory/NatIso.lean

@@ -65,6 +65,16 @@ theorem inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
     α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
   congr_fun (congr_arg NatTrans.app α.inv_hom_id) X
 
+@[reassoc (attr := simp)]
+lemma hom_inv_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
+    (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 _ := by
+  rw [← NatTrans.comp_app, Iso.hom_inv_id_app, NatTrans.id_app]
+
+@[reassoc (attr := simp)]
+lemma inv_hom_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
+    (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 _ := by
+  rw [← NatTrans.comp_app, Iso.inv_hom_id_app, NatTrans.id_app]
+
 end Iso
 
 namespace NatIso

Mathlib/CategoryTheory/Whiskering.lean

@@ -302,4 +302,20 @@ theorem pentagon :
 
 end Functor
 
+variable {C₁ C₂ D₁ D₂ : Type*} [Category C₁] [Category C₂]
+  [Category D₁] [Category D₂] (E : Type*) [Category E]
+
+/-- The obvious functor `(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E)`. -/
+@[simps!]
+def whiskeringLeft₂ :
+    (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E) where
+  obj F₁ :=
+    { obj := fun F₂ ↦
+        (whiskeringRight D₁ (D₂ ⥤ E) (C₂ ⥤ E)).obj ((whiskeringLeft C₂ D₂ E).obj F₂) ⋙
+          (whiskeringLeft C₁ D₁ (C₂ ⥤ E)).obj F₁
+      map := fun φ ↦ whiskerRight
+        ((whiskeringRight D₁ (D₂ ⥤ E) (C₂ ⥤ E)).map ((whiskeringLeft C₂ D₂ E).map φ)) _ }
+  map ψ :=
+    { app := fun F₂ ↦ whiskerLeft _ ((whiskeringLeft C₁ D₁ (C₂ ⥤ E)).map ψ) }
+
 end CategoryTheory