feat(CategoryTheory): the localized category of a product category (#…

…8516)

This PR develops the API for cartesian products of categories (natural isomorphisms, equivalences, morphism properties) in order to show that under simple assumptions, the localized category of a product of two categories identifies to a product of the localized categories.

Mathlib.lean

@@ -1130,6 +1130,7 @@ import Mathlib.CategoryTheory.Localization.Equivalence
 import Mathlib.CategoryTheory.Localization.LocalizerMorphism
 import Mathlib.CategoryTheory.Localization.Opposite
 import Mathlib.CategoryTheory.Localization.Predicate
+import Mathlib.CategoryTheory.Localization.Prod
 import Mathlib.CategoryTheory.Monad.Adjunction
 import Mathlib.CategoryTheory.Monad.Algebra
 import Mathlib.CategoryTheory.Monad.Basic

Mathlib/CategoryTheory/Functor/Currying.lean

@@ -19,10 +19,10 @@ and verify that they provide an equivalence of categories
 
 namespace CategoryTheory
 
-universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+universe v₁ v₂ v₃ v₄ v₅ u₁ u₂ u₃ u₄ u₅
 
 variable {B : Type u₁} [Category.{v₁} B] {C : Type u₂} [Category.{v₂} C] {D : Type u₃}
-  [Category.{v₃} D] {E : Type u₄} [Category.{v₄} E]
+  [Category.{v₃} D] {E : Type u₄} [Category.{v₄} E] {H : Type u₅} [Category.{v₅} H]
 
 /-- The uncurrying functor, taking a functor `C ⥤ (D ⥤ E)` and producing a functor `(C × D) ⥤ E`.
 -/
@@ -115,4 +115,44 @@ def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E
     whiskeringRight _ _ _ ⋙ (whiskeringLeft _ _ _).obj (prodFunctorToFunctorProd _ _ _) ⋙ curry
 #align category_theory.whiskering_right₂ CategoryTheory.whiskeringRight₂
 
+namespace Functor
+
+variable {B C D E}
+
+lemma uncurry_obj_curry_obj (F : B × C ⥤ D) : uncurry.obj (curry.obj F) = F :=
+  Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
+    dsimp
+    simp only [← F.map_comp, Category.id_comp, Category.comp_id, prod_comp])
+
+lemma curry_obj_injective {F₁ F₂ : C × D ⥤ E} (h : curry.obj F₁ = curry.obj F₂) :
+    F₁ = F₂ := by
+  rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]
+
+lemma curry_obj_uncurry_obj (F : B ⥤ C ⥤ D) : curry.obj (uncurry.obj F) = F :=
+  Functor.ext (fun _ => Functor.ext (by simp) (by simp)) (by aesop_cat)
+
+lemma uncurry_obj_injective {F₁ F₂ : B ⥤ C ⥤ D} (h : uncurry.obj F₁ = uncurry.obj F₂) :
+    F₁ = F₂ := by
+  rw [← curry_obj_uncurry_obj F₁, ← curry_obj_uncurry_obj F₂, h]
+
+lemma flip_flip (F : B ⥤ C ⥤ D) : F.flip.flip = F := rfl
+
+lemma flip_injective {F₁ F₂ : B ⥤ C ⥤ D} (h : F₁.flip = F₂.flip) :
+    F₁ = F₂ := by
+  rw [← flip_flip F₁, ← flip_flip F₂, h]
+
+lemma uncurry_obj_curry_obj_flip_flip (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
+    uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip = (F₁.prod F₂) ⋙ G :=
+  Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
+    dsimp
+    simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])
+
+lemma uncurry_obj_curry_obj_flip_flip' (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
+    uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip) = (F₁.prod F₂) ⋙ G :=
+  Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
+    dsimp
+    simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])
+
+end Functor
+
 end CategoryTheory

Mathlib/CategoryTheory/Localization/Prod.lean

@@ -0,0 +1,136 @@
+/-
+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.Equivalence
+
+/-!
+# Localization of product categories
+
+In this file, it is shown that if functors `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂`
+are localization functors for morphisms properties `W₁` and `W₂`, then
+the product functor `C₁ × C₂ ⥤ D₁ × D₂` is a localization functor for
+`W₁.prod W₂ : MorphismProperty (C₁ × C₂)`, at least if both `W₁` and `W₂`
+contain identities. This main result is the instance `Functor.IsLocalization.prod`.
+
+The proof proceeds by showing first `Localization.Construction.prodIsLocalization`,
+which asserts that this holds for the localization functors `W₁.Q` and `W₂.Q` to
+the constructed localized categories: this is done by showing that the product
+functor `W₁.Q.prod W₂.Q : C₁ × C₂ ⥤ W₁.Localization × W₂.Localization` satisfies
+the strict universal property of the localization for `W₁.prod W₂`. The general
+case follows by transporting this result through equivalences of categories.
+
+-/
+
+universe v₁ v₂ v₃ v₄ v₅ u₁ u₂ u₃ u₄ u₅
+
+namespace CategoryTheory
+
+variable {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₃} {D₂ : Type u₄}
+  [Category.{v₁} C₁] [Category.{v₂} C₂] [Category.{v₃} D₁] [Category.{v₄} D₂]
+  (L₁ : C₁ ⥤ D₁) {W₁ : MorphismProperty C₁} [W₁.ContainsIdentities]
+  (L₂ : C₂ ⥤ D₂) {W₂ : MorphismProperty C₂} [W₂.ContainsIdentities]
+
+namespace Localization
+
+namespace StrictUniversalPropertyFixedTarget
+
+variable {E : Type u₅} [Category.{v₅} E]
+  (F : C₁ × C₂ ⥤ E) (hF : (W₁.prod W₂).IsInvertedBy F)
+
+/-- Auxiliary definition for `prodLift`. -/
+noncomputable def prodLift₁ :
+    W₁.Localization ⥤ C₂ ⥤ E :=
+  Construction.lift (curry.obj F) (fun _ _ f₁ hf₁ => by
+    haveI : ∀ (X₂ : C₂), IsIso (((curry.obj F).map f₁).app X₂) :=
+      fun X₂ => hF _ ⟨hf₁, MorphismProperty.id_mem _ _⟩
+    apply NatIso.isIso_of_isIso_app)
+
+lemma prod_fac₁ :
+    W₁.Q ⋙ prodLift₁ F hF = curry.obj F :=
+  Construction.fac _ _
+
+/-- The lifting of a functor `F : C₁ × C₂ ⥤ E` inverting `W₁.prod W₂` to a functor
+`W₁.Localization × W₂.Localization ⥤ E` -/
+noncomputable def prodLift :
+    W₁.Localization × W₂.Localization ⥤ E := by
+  refine' uncurry.obj (Construction.lift (prodLift₁ F hF).flip _).flip
+  intro _ _ f₂ hf₂
+  haveI : ∀ (X₁ : W₁.Localization),
+      IsIso (((Functor.flip (prodLift₁ F hF)).map f₂).app X₁) := fun X₁ => by
+    obtain ⟨X₁, rfl⟩ := (Construction.objEquiv W₁).surjective X₁
+    exact ((MorphismProperty.RespectsIso.isomorphisms E).arrow_mk_iso_iff
+      (((Functor.mapArrowFunctor _ _).mapIso
+        (eqToIso (Functor.congr_obj (prod_fac₁ F hF) X₁))).app (Arrow.mk f₂))).2
+          (hF _ ⟨MorphismProperty.id_mem _ _, hf₂⟩)
+  apply NatIso.isIso_of_isIso_app
+
+lemma prod_fac₂ :
+    W₂.Q ⋙ (curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip := by
+  simp only [prodLift, Functor.curry_obj_uncurry_obj, Functor.flip_flip]
+  apply Construction.fac
+
+lemma prod_fac :
+    (W₁.Q.prod W₂.Q) ⋙ prodLift F hF = F := by
+  rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
+    Functor.uncurry_obj_curry_obj]
+
+lemma prod_uniq (F₁ F₂ : (W₁.Localization × W₂.Localization ⥤ E))
+    (h : (W₁.Q.prod W₂.Q) ⋙ F₁ = (W₁.Q.prod W₂.Q) ⋙ F₂) :
+      F₁ = F₂ := by
+  apply Functor.curry_obj_injective
+  apply Construction.uniq
+  apply Functor.flip_injective
+  apply Construction.uniq
+  apply Functor.flip_injective
+  apply Functor.uncurry_obj_injective
+  simpa only [Functor.uncurry_obj_curry_obj_flip_flip] using h
+
+variable (W₁ W₂)
+
+/-- The product of two (constructed) localized categories satisfies the universal
+property of the localized category of the product. -/
+noncomputable def prod :
+    StrictUniversalPropertyFixedTarget (W₁.Q.prod W₂.Q) (W₁.prod W₂) E where
+  inverts := (Localization.inverts W₁.Q W₁).prod (Localization.inverts W₂.Q W₂)
+  lift := prodLift
+  fac := prod_fac
+  uniq := prod_uniq
+
+end StrictUniversalPropertyFixedTarget
+
+variable (W₁ W₂)
+
+lemma Construction.prodIsLocalization :
+    (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂) :=
+  Functor.IsLocalization.mk' _ _
+    (StrictUniversalPropertyFixedTarget.prod W₁ W₂)
+    (StrictUniversalPropertyFixedTarget.prod W₁ W₂)
+
+end Localization
+
+open Localization
+
+namespace Functor
+
+namespace IsLocalization
+
+variable (W₁ W₂)
+
+/-- If `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` are localization functors
+for `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂` respectively,
+and if both `W₁` and `W₂` contain identites, then the product
+functor `L₁.prod L₂ : C₁ × C₂ ⥤ D₁ × D₂` is a localization functor for `W₁.prod W₂`. -/
+instance prod [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] :
+    (L₁.prod L₂).IsLocalization (W₁.prod W₂) := by
+  haveI := Construction.prodIsLocalization W₁ W₂
+  exact of_equivalence_target (W₁.Q.prod W₂.Q) (W₁.prod W₂) (L₁.prod L₂)
+    ((uniq W₁.Q L₁ W₁).prod (uniq W₂.Q L₂ W₂))
+    (NatIso.prod (compUniqFunctor W₁.Q L₁ W₁) (compUniqFunctor W₂.Q L₂ W₂))
+
+end IsLocalization
+
+end Functor
+
+end CategoryTheory

Mathlib/CategoryTheory/MorphismProperty.lean

@@ -917,6 +917,29 @@ lemma of_unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W.unop] : IsMulti
 
 end IsMultiplicative
 
+section
+
+variable {C₁ C₂ : Type*} [Category C₁] [Category C₂]
+
+/-- If `W₁` and `W₂` are morphism properties on two categories `C₁` and `C₂`,
+this is the induced morphism property on `C₁ × C₂`. -/
+def prod (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) :
+    MorphismProperty (C₁ × C₂) :=
+  fun _ _ f => W₁ f.1 ∧ W₂ f.2
+
+instance Prod.containsIdentities (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂)
+    [W₁.ContainsIdentities] [W₂.ContainsIdentities] : (prod W₁ W₂).ContainsIdentities :=
+  ⟨fun _ => ⟨W₁.id_mem _, W₂.id_mem _⟩⟩
+
+lemma IsInvertedBy.prod {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂}
+    {E₁ E₂ : Type*} [Category E₁] [Category E₂] {F₁ : C₁ ⥤ E₁} {F₂ : C₂ ⥤ E₂}
+    (h₁ : W₁.IsInvertedBy F₁) (h₂ : W₂.IsInvertedBy F₂) :
+    (W₁.prod W₂).IsInvertedBy (F₁.prod F₂) := fun _ _ f hf => by
+  rw [isIso_prod_iff]
+  exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩
+
+end
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/Products/Basic.lean

@@ -298,6 +298,29 @@ def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.prod
    use instead `α.prod β` or `NatTrans.prod α β`. -/
 end NatTrans
 
+namespace NatIso
+
+/-- The cartesian product of two natural isomorphisms. -/
+@[simps]
+def prod {F F' : A ⥤ B} {G G' : C ⥤ D} (e₁ : F ≅ F') (e₂ : G ≅ G') :
+    F.prod G ≅ F'.prod G' where
+  hom := NatTrans.prod e₁.hom e₂.hom
+  inv := NatTrans.prod e₁.inv e₂.inv
+
+end NatIso
+
+namespace Equivalence
+
+/-- The cartesian product of two equivalences of categories. -/
+@[simps]
+def prod (E₁ : A ≌ B) (E₂ : C ≌ D) : A × C ≌ B × D where
+  functor := E₁.functor.prod E₂.functor
+  inverse := E₁.inverse.prod E₂.inverse
+  unitIso := NatIso.prod E₁.unitIso E₂.unitIso
+  counitIso := NatIso.prod E₁.counitIso E₂.counitIso
+
+end Equivalence
+
 /-- `F.flip` composed with evaluation is the same as evaluating `F`. -/
 @[simps!]
 def flipCompEvaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a ≅ F.obj a :=