From 9ce2706ba0550a9d9704e926a250064a9d30e6ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 6 Dec 2023 19:48:14 +0100
Subject: [PATCH 1/6] feat(CategoryTheory): localization of product categories

---
 Mathlib.lean                                 |   1 +
 Mathlib/CategoryTheory/Localization/Pi.lean  | 107 +++++++++++++++++++
 Mathlib/CategoryTheory/MorphismProperty.lean |  25 ++++-
 Mathlib/CategoryTheory/Pi/Basic.lean         |  14 ++-
 4 files changed, 144 insertions(+), 3 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/Localization/Pi.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 509febe15a0df..5fe3355e0b8ef 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1135,6 +1135,7 @@ import Mathlib.CategoryTheory.Localization.Construction
 import Mathlib.CategoryTheory.Localization.Equivalence
 import Mathlib.CategoryTheory.Localization.LocalizerMorphism
 import Mathlib.CategoryTheory.Localization.Opposite
+import Mathlib.CategoryTheory.Localization.Pi
 import Mathlib.CategoryTheory.Localization.Predicate
 import Mathlib.CategoryTheory.Localization.Prod
 import Mathlib.CategoryTheory.Monad.Adjunction
diff --git a/Mathlib/CategoryTheory/Localization/Pi.lean b/Mathlib/CategoryTheory/Localization/Pi.lean
new file mode 100644
index 0000000000000..b939e84b3092b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Localization/Pi.lean
@@ -0,0 +1,107 @@
+/-
+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
+
+/-!
+# Localization of product categories
+
+In this file, it is shown that if for all `j : J` (with `J` finite),
+functors `L j : C j ⥤ D j` are localization functors with respect
+to a class of morphism `W j : MorphismProperty (C j)`, then the product
+functor `Functor.pi L : (∀ j, C j) ⥤ ∀ j, D j` is a localization
+functor for the product class of morphism `MorphismProperty.pi W`.
+The proof proceeds by induction on the cardinal of `J` using the
+main result of `Mathlib.CategoryTheory.Localization.Pi`.
+
+-/
+
+universe v₁ v₂ v₃ u₀ u₁ u₂ u₃ u₄
+
+namespace CategoryTheory
+
+variable (J : Type u₀) (C : J → Type u₁) {D : J → Type u₂}
+  [∀ j, Category.{v₁} (C j)] [∀ j, Category.{v₂} (D j)]
+  (L : ∀ j, C j ⥤ D j) (W : ∀ j, MorphismProperty (C j))
+  [∀ j, (W j).ContainsIdentities]
+  [∀ j, (L j).IsLocalization (W j)]
+
+namespace Functor
+
+namespace IsLocalization
+
+instance pi [Finite J] :
+    (Functor.pi L).IsLocalization (MorphismProperty.pi W) := by
+  let P : Type u₀ → Prop := fun J => ∀ {C : J → Type u₁} {D : J → Type u₂}
+    [∀ j, Category.{v₁} (C j)] [∀ j, Category.{v₂} (D j)]
+    (L : ∀ j, C j ⥤ D j) (W : ∀ j, MorphismProperty (C j))
+    [∀ j, (W j).ContainsIdentities] [∀ j, (L j).IsLocalization (W j)],
+      (Functor.pi L).IsLocalization (MorphismProperty.pi W)
+  suffices P J
+    by apply this
+  apply @Finite.induction_empty_option P
+  · intro J₁ J₂ e hJ₁ C₂ D₂ hC₂ _ L₂ W₂ _ _
+    let C₁ := fun j => (C₂ (e j))
+    let D₁ := fun j => (D₂ (e j))
+    let L₁ : ∀ j, C₁ j ⥤ D₁ j := fun j => (L₂ (e j))
+    let W₁ : ∀ j, MorphismProperty (C₁ j) := fun j => (W₂ (e j))
+    replace hJ₁ := hJ₁ L₁ W₁
+    letI : ∀ i, Category (C₂ i) := by apply hC₂
+    let E := pi_equivalence_of_equiv C₂ e
+    let E' := pi_equivalence_of_equiv D₂ e
+    haveI : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor :=
+      (CatCommSq.hInvEquiv E (Functor.pi L₁) (Functor.pi L₂) E').symm ⟨Iso.refl _⟩
+    refine' IsLocalization.of_equivalences (Functor.pi L₁)
+      (MorphismProperty.pi W₁) (Functor.pi L₂) (MorphismProperty.pi W₂) E E' _
+      (MorphismProperty.IsInvertedBy.pi _ _ (fun j => Localization.inverts _ _))
+    intro _ _ f hf
+    refine' ⟨_, _, E.functor.map f, _, ⟨Iso.refl _⟩⟩
+    intro i
+    have hf' := hf (e.symm i)
+    dsimp
+    have H : ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y) (_ : W₂ j g),
+        W₂ j' ((Pi.equivalence_of_eq C₂ h).functor.map g) := by
+      rintro j _ rfl _ _ g hg
+      exact hg
+    exact H (e.apply_symm_apply i) _ hf'
+  · intro C D _ _ L W _ _
+    haveI : ∀ j, IsEquivalence (L j) := by rintro ⟨⟩
+    refine' of_equivalence _ _ (fun _ _ _ _ => _)
+    rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]
+    rintro ⟨⟩
+  · intro J _ hJ C D _ _ L W _ _
+    let C' := fun j => C (some j)
+    let D' := fun j => D (some j)
+    let L' : ∀ j, C' j ⥤ D' j := fun j => L (some j)
+    let W' : ∀ j, MorphismProperty (C' j) := fun j => W (some j)
+    replace hJ := hJ L' W'
+    haveI : IsLocalization ((L none).prod (Functor.pi L'))
+      ((W none).prod (MorphismProperty.pi W')) := inferInstance
+    let L₁ := (L none).prod (Functor.pi L')
+    let L₂ := Functor.pi L
+    let W₁ := (W none).prod (MorphismProperty.pi W')
+    let W₂ := MorphismProperty.pi W
+    haveI : CatCommSq (pi_option_equivalence C).symm.functor L₁ L₂
+      (pi_option_equivalence D).symm.functor :=
+        ⟨NatIso.pi' (by rintro (_|i) <;> apply Iso.refl)⟩
+    refine' IsLocalization.of_equivalences L₁ W₁ L₂ W₂
+      (pi_option_equivalence C).symm (pi_option_equivalence D).symm _ _
+    · intro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ f ⟨hf₁, hf₂⟩
+      refine' ⟨_, _, (pi_option_equivalence C).inverse.map f, _, ⟨Iso.refl _⟩⟩
+      · rintro (_|i)
+        · exact hf₁
+        · apply hf₂
+    · apply MorphismProperty.IsInvertedBy.pi
+      rintro (_|i) <;> apply Localization.inverts
+
+instance pi' [Finite J] :
+    (Functor.pi (fun j => (W j).Q)).IsLocalization (MorphismProperty.pi W) :=
+  inferInstance
+
+end IsLocalization
+
+end Functor
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/MorphismProperty.lean b/Mathlib/CategoryTheory/MorphismProperty.lean
index e476dd85e191f..115c322ddee0a 100644
--- a/Mathlib/CategoryTheory/MorphismProperty.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty.lean
@@ -27,7 +27,7 @@ The following meta-properties are defined
 -/
 
 
-universe v u
+universe w v v' u u'
 
 open CategoryTheory CategoryTheory.Limits Opposite
 
@@ -940,6 +940,29 @@ lemma IsInvertedBy.prod {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty
 
 end
 
+section
+
+variable {J : Type w} {C : J → Type u} {D : J → Type u'}
+  [∀ j, Category.{v} (C j)] [∀ j, Category.{v'} (D j)]
+  (W : ∀ j, MorphismProperty (C j))
+
+/-- If `W j` are morphism properties on categories `C j` for all `j`, this is the
+induced morphism property on the category `∀ j, C j`. -/
+def pi : MorphismProperty (∀ j, C j) := fun _ _ f => ∀ j, (W j) (f j)
+
+instance Pi.containsIdentities [∀ j, (W j).ContainsIdentities] :
+    (pi W).ContainsIdentities :=
+  ⟨fun _ _ => MorphismProperty.id_mem _ _⟩
+
+lemma IsInvertedBy.pi (F : ∀ j, C j ⥤ D j) (hF : ∀ j, (W j).IsInvertedBy (F j)) :
+    (MorphismProperty.pi W).IsInvertedBy (Functor.pi F) := by
+  intro _ _ f hf
+  rw [isIso_pi_iff]
+  intro j
+  exact hF j _ (hf j)
+
+end
+
 end MorphismProperty
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index b7f7dd1b17a03..05a4435c4d828 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -19,7 +19,7 @@ We define the pointwise category structure on indexed families of objects in a c
 
 namespace CategoryTheory
 
-universe w₀ w₁ w₂ v₁ v₂ u₁ u₂
+universe w₀ w₁ w₂ v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [∀ i, Category.{v₁} (C i)]
 
@@ -198,7 +198,7 @@ namespace Functor
 
 variable {C}
 
-variable {D : I → Type u₁} [∀ i, Category.{v₁} (D i)] {A : Type u₁} [Category.{u₁} A]
+variable {D : I → Type u₂} [∀ i, Category.{v₂} (D i)] {A : Type u₃} [Category.{v₃} A]
 
 /-- Assemble an `I`-indexed family of functors into a functor between the pi types.
 -/
@@ -274,4 +274,14 @@ def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where
 
 end NatTrans
 
+variable {C}
+
+lemma isIso_pi_iff {X Y : ∀ i, C i} (f : X ⟶ Y) :
+    IsIso f ↔ ∀ i, IsIso (f i) := by
+  constructor
+  · intro _ i
+    exact IsIso.of_iso (Pi.isoApp (asIso f) i)
+  · intro
+    exact ⟨fun i => inv (f i), by aesop_cat, by aesop_cat⟩
+
 end CategoryTheory

From 7355dfa138e623ce4ddf3d66d9fa9ea604251238 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 7 Dec 2023 11:03:24 +0100
Subject: [PATCH 2/6] fixed the build

---
 Mathlib/CategoryTheory/Localization/Pi.lean   |  75 ++++-------
 .../Localization/Predicate.lean               |   6 +
 Mathlib/CategoryTheory/Pi/Basic.lean          | 118 +++++++++++++++++-
 3 files changed, 145 insertions(+), 54 deletions(-)

diff --git a/Mathlib/CategoryTheory/Localization/Pi.lean b/Mathlib/CategoryTheory/Localization/Pi.lean
index b939e84b3092b..4cd04799b021f 100644
--- a/Mathlib/CategoryTheory/Localization/Pi.lean
+++ b/Mathlib/CategoryTheory/Localization/Pi.lean
@@ -14,61 +14,44 @@ to a class of morphism `W j : MorphismProperty (C j)`, then the product
 functor `Functor.pi L : (∀ j, C j) ⥤ ∀ j, D j` is a localization
 functor for the product class of morphism `MorphismProperty.pi W`.
 The proof proceeds by induction on the cardinal of `J` using the
-main result of `Mathlib.CategoryTheory.Localization.Pi`.
+main result of the file `Mathlib.CategoryTheory.Localization.Prod`.
 
 -/
 
-universe v₁ v₂ v₃ u₀ u₁ u₂ u₃ u₄
+universe w v₁ v₂ u₁ u₂
 
-namespace CategoryTheory
+namespace CategoryTheory.Functor.IsLocalization
 
-variable (J : Type u₀) (C : J → Type u₁) {D : J → Type u₂}
+instance pi {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂}
   [∀ j, Category.{v₁} (C j)] [∀ j, Category.{v₂} (D j)]
   (L : ∀ j, C j ⥤ D j) (W : ∀ j, MorphismProperty (C j))
-  [∀ j, (W j).ContainsIdentities]
-  [∀ j, (L j).IsLocalization (W j)]
-
-namespace Functor
-
-namespace IsLocalization
-
-instance pi [Finite J] :
+  [∀ j, (W j).ContainsIdentities] [∀ j, (L j).IsLocalization (W j)] :
     (Functor.pi L).IsLocalization (MorphismProperty.pi W) := by
-  let P : Type u₀ → Prop := fun J => ∀ {C : J → Type u₁} {D : J → Type u₂}
-    [∀ j, Category.{v₁} (C j)] [∀ j, Category.{v₂} (D j)]
-    (L : ∀ j, C j ⥤ D j) (W : ∀ j, MorphismProperty (C j))
-    [∀ j, (W j).ContainsIdentities] [∀ j, (L j).IsLocalization (W j)],
-      (Functor.pi L).IsLocalization (MorphismProperty.pi W)
-  suffices P J
-    by apply this
-  apply @Finite.induction_empty_option P
-  · intro J₁ J₂ e hJ₁ C₂ D₂ hC₂ _ L₂ W₂ _ _
+  revert J
+  apply Finite.induction_empty_option
+  · intro J₁ J₂ e hJ₁ C₂ D₂ _ _ L₂ W₂ _ _
     let C₁ := fun j => (C₂ (e j))
     let D₁ := fun j => (D₂ (e j))
     let L₁ : ∀ j, C₁ j ⥤ D₁ j := fun j => (L₂ (e j))
     let W₁ : ∀ j, MorphismProperty (C₁ j) := fun j => (W₂ (e j))
     replace hJ₁ := hJ₁ L₁ W₁
-    letI : ∀ i, Category (C₂ i) := by apply hC₂
-    let E := pi_equivalence_of_equiv C₂ e
-    let E' := pi_equivalence_of_equiv D₂ e
+    let E := Pi.equivalenceOfEquiv C₂ e
+    let E' := Pi.equivalenceOfEquiv D₂ e
     haveI : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor :=
       (CatCommSq.hInvEquiv E (Functor.pi L₁) (Functor.pi L₂) E').symm ⟨Iso.refl _⟩
-    refine' IsLocalization.of_equivalences (Functor.pi L₁)
-      (MorphismProperty.pi W₁) (Functor.pi L₂) (MorphismProperty.pi W₂) E E' _
-      (MorphismProperty.IsInvertedBy.pi _ _ (fun j => Localization.inverts _ _))
+    refine IsLocalization.of_equivalences (Functor.pi L₁)
+      (MorphismProperty.pi W₁) (Functor.pi L₂) (MorphismProperty.pi W₂) E E' ?_
+      (MorphismProperty.IsInvertedBy.pi _ _ (fun _ => Localization.inverts _ _))
     intro _ _ f hf
-    refine' ⟨_, _, E.functor.map f, _, ⟨Iso.refl _⟩⟩
-    intro i
-    have hf' := hf (e.symm i)
-    dsimp
+    refine ⟨_, _, E.functor.map f, fun i => ?_, ⟨Iso.refl _⟩⟩
     have H : ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y) (_ : W₂ j g),
-        W₂ j' ((Pi.equivalence_of_eq C₂ h).functor.map g) := by
+        W₂ j' ((Pi.eqToEquivalence C₂ h).functor.map g) := by
       rintro j _ rfl _ _ g hg
       exact hg
-    exact H (e.apply_symm_apply i) _ hf'
+    exact H (e.apply_symm_apply i) _ (hf (e.symm i))
   · intro C D _ _ L W _ _
     haveI : ∀ j, IsEquivalence (L j) := by rintro ⟨⟩
-    refine' of_equivalence _ _ (fun _ _ _ _ => _)
+    refine IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)
     rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]
     rintro ⟨⟩
   · intro J _ hJ C D _ _ L W _ _
@@ -77,31 +60,19 @@ instance pi [Finite J] :
     let L' : ∀ j, C' j ⥤ D' j := fun j => L (some j)
     let W' : ∀ j, MorphismProperty (C' j) := fun j => W (some j)
     replace hJ := hJ L' W'
-    haveI : IsLocalization ((L none).prod (Functor.pi L'))
-      ((W none).prod (MorphismProperty.pi W')) := inferInstance
     let L₁ := (L none).prod (Functor.pi L')
     let L₂ := Functor.pi L
-    let W₁ := (W none).prod (MorphismProperty.pi W')
-    let W₂ := MorphismProperty.pi W
-    haveI : CatCommSq (pi_option_equivalence C).symm.functor L₁ L₂
-      (pi_option_equivalence D).symm.functor :=
+    haveI : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ L₂
+      (Pi.optionEquivalence D).symm.functor :=
         ⟨NatIso.pi' (by rintro (_|i) <;> apply Iso.refl)⟩
-    refine' IsLocalization.of_equivalences L₁ W₁ L₂ W₂
-      (pi_option_equivalence C).symm (pi_option_equivalence D).symm _ _
+    refine IsLocalization.of_equivalences L₁ ((W none).prod (MorphismProperty.pi W')) L₂ _
+      (Pi.optionEquivalence C).symm (Pi.optionEquivalence D).symm ?_ ?_
     · intro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ f ⟨hf₁, hf₂⟩
-      refine' ⟨_, _, (pi_option_equivalence C).inverse.map f, _, ⟨Iso.refl _⟩⟩
+      refine ⟨_, _, (Pi.optionEquivalence C).inverse.map f, ?_, ⟨Iso.refl _⟩⟩
       · rintro (_|i)
         · exact hf₁
         · apply hf₂
     · apply MorphismProperty.IsInvertedBy.pi
       rintro (_|i) <;> apply Localization.inverts
 
-instance pi' [Finite J] :
-    (Functor.pi (fun j => (W j).Q)).IsLocalization (MorphismProperty.pi W) :=
-  inferInstance
-
-end IsLocalization
-
-end Functor
-
-end CategoryTheory
+end CategoryTheory.Functor.IsLocalization
diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean
index a059c145afd76..bde3a8e3310a1 100644
--- a/Mathlib/CategoryTheory/Localization/Predicate.lean
+++ b/Mathlib/CategoryTheory/Localization/Predicate.lean
@@ -434,6 +434,12 @@ theorem of_equivalence_target {E : Type*} [Category E] (L' : C ⥤ E) (eq : D 
       nonempty_isEquivalence := Nonempty.intro (IsEquivalence.ofIso e' inferInstance) }
 #align category_theory.functor.is_localization.of_equivalence_target CategoryTheory.Functor.IsLocalization.of_equivalence_target
 
+lemma of_isEquivalence (L : C ⥤ D) (W : MorphismProperty C)
+    (hW : W ⊆ MorphismProperty.isomorphisms C) [IsEquivalence L] :
+    L.IsLocalization W := by
+  haveI : (𝟭 C).IsLocalization W := for_id W hW
+  exact of_equivalence_target (𝟭 C) W L L.asEquivalence L.leftUnitor
+
 end IsLocalization
 
 end Functor
diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index 05a4435c4d828..d03c834aa6798 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -3,8 +3,9 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Scott Morrison
 -/
-import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.EqToHom
+import Mathlib.CategoryTheory.NatIso
+import Mathlib.CategoryTheory.Products.Basic
 import Mathlib.Data.Sum.Basic
 
 #align_import category_theory.pi.basic from "leanprover-community/mathlib"@"dc6c365e751e34d100e80fe6e314c3c3e0fd2988"
@@ -216,6 +217,12 @@ def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i where
   map h i := (f i).map h
 #align category_theory.functor.pi' CategoryTheory.Functor.pi'
 
+/-- The projections of `Functor.pi' F` are isomorphic to the functors of the family `F` -/
+@[simps!]
+def pi'CompEval {A : Type*} [Category A] (F : ∀ i, A ⥤ C i) (i : I) :
+    pi' F ⋙ Pi.eval C i ≅ F i :=
+  Iso.refl _
+
 section EqToHom
 
 @[simp]
@@ -261,7 +268,7 @@ namespace NatTrans
 
 variable {C}
 
-variable {D : I → Type u₁} [∀ i, Category.{v₁} (D i)]
+variable {D : I → Type u₂} [∀ i, Category.{v₂} (D i)]
 
 variable {F G : ∀ i, C i ⥤ D i}
 
@@ -272,8 +279,41 @@ def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where
   app f i := (α i).app (f i)
 #align category_theory.nat_trans.pi CategoryTheory.NatTrans.pi
 
+/-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
+-/
+@[simps]
+def pi' {E : Type*} [Category E] {F G : E ⥤ ∀ i, C i}
+    (τ : ∀ i, F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i) : F ⟶ G where
+  app := fun X i => (τ i).app X
+  naturality _ _ f := by
+    ext i
+    exact (τ i).naturality f
+
 end NatTrans
 
+namespace NatIso
+
+variable {C}
+variable {D : I → Type u₂} [∀ i, Category.{v₂} (D i)]
+variable {F G : ∀ i, C i ⥤ D i}
+
+/-- Assemble an `I`-indexed family of natural isomorphisms into a single natural isomorphism.
+-/
+@[simps]
+def pi (e : ∀ i, F i ≅ G i) : Functor.pi F ≅ Functor.pi G where
+  hom := NatTrans.pi (fun i => (e i).hom)
+  inv := NatTrans.pi (fun i => (e i).inv)
+
+/-- Assemble an `I`-indexed family of natural isomorphisms into a single natural isomorphism.
+-/
+@[simps]
+def pi' {E : Type*} [Category E] {F G : E ⥤ ∀ i, C i}
+    (e : ∀ i, F ⋙ Pi.eval C i ≅ G ⋙ Pi.eval C i) : F ≅ G where
+  hom := NatTrans.pi' (fun i => (e i).hom)
+  inv := NatTrans.pi' (fun i => (e i).inv)
+
+end NatIso
+
 variable {C}
 
 lemma isIso_pi_iff {X Y : ∀ i, C i} (f : X ⟶ Y) :
@@ -284,4 +324,78 @@ lemma isIso_pi_iff {X Y : ∀ i, C i} (f : X ⟶ Y) :
   · intro
     exact ⟨fun i => inv (f i), by aesop_cat, by aesop_cat⟩
 
+variable (C)
+
+/-- For a family of categories `C i` indexed by `I`, an equality `i = j` in `I` induces
+an equivalence `C i ≌ C j`. -/
+def Pi.eqToEquivalence {i j : I} (h : i = j) : C i ≌ C j := by subst h; rfl
+
+/-- When `i = j`, projections `Pi.eval C i` and `Pi.eval C j` are related by the equivalence
+`Pi.eqToEquivalence C h : C i ≌ C j`. -/
+@[simps!]
+def Pi.evalCompEqToEquivalenceFunctor {i j : I} (h : i = j) :
+    Pi.eval C i ⋙ (Pi.eqToEquivalence C h).functor ≅
+      Pi.eval C j :=
+  eqToIso (by subst h; rfl)
+
+/-- The equivalences given by `Pi.eqToEquivalence` are compatible with reindexing. -/
+@[simps!]
+def Pi.eqToEquivalenceFunctorIso (f : J → I) {i' j' : J} (h : i' = j') :
+    (Pi.eqToEquivalence C (congr_arg f h)).functor ≅
+      (Pi.eqToEquivalence (fun i' => C (f i')) h).functor :=
+  eqToIso (by subst h; rfl)
+
+attribute [local simp] eqToHom_map
+
+/-- Reindexing a family of categories gives equivalent `Pi` categories. -/
+@[simps]
+noncomputable def Pi.equivalenceOfEquiv (e : J ≃ I) :
+    (∀ j, C (e j)) ≌ (∀ i, C i) where
+  functor := Functor.pi' (fun i => Pi.eval _ (e.symm i) ⋙
+    (Pi.eqToEquivalence C (by simp)).functor)
+  inverse := Functor.pi' (fun i' => Pi.eval _ (e i'))
+  unitIso := NatIso.pi' (fun i' => Functor.leftUnitor _ ≪≫
+    (Pi.evalCompEqToEquivalenceFunctor (fun j => C (e j)) (e.symm_apply_apply i')).symm ≪≫
+    isoWhiskerLeft _ ((Pi.eqToEquivalenceFunctorIso C e (e.symm_apply_apply i')).symm) ≪≫
+    (Functor.pi'CompEval _ _).symm ≪≫ isoWhiskerLeft _ (Functor.pi'CompEval _ _).symm ≪≫
+    (Functor.associator _ _ _).symm)
+  counitIso := NatIso.pi' (fun i => (Functor.associator _ _ _).symm ≪≫
+    isoWhiskerRight (Functor.pi'CompEval _ _) _ ≪≫
+    Pi.evalCompEqToEquivalenceFunctor C (e.apply_symm_apply i) ≪≫
+    (Functor.leftUnitor _).symm)
+
+/-- A product of categories indexed by `Option J` identifies to a binary product. -/
+@[simps!]
+def Pi.optionEquivalence (C' : Option J → Type u₁) [∀ i, Category.{v₁} (C' i)] :
+    (∀ i, C' i) ≌ C' none × (∀ (j : J), C' (some j)) where
+  functor := Functor.prod' (Pi.eval C' none)
+    (Functor.pi' (fun i => (Pi.eval _ (some i))))
+  inverse := Functor.pi' (fun i => match i with
+    | none => Prod.fst _ _
+    | some i => Prod.snd _ _ ⋙ (Pi.eval _ i))
+  unitIso :=  NatIso.pi' (fun i => match i with
+    | none => Iso.refl _
+    | some i => Iso.refl _)
+  counitIso := by exact Iso.refl _
+
+namespace Equivalence
+
+variable {C}
+variable {D : I → Type u₂} [∀ i, Category.{v₂} (D i)]
+
+/-- Assemble an `I`-indexed family of equivalences of categories isomorphisms
+into a single equivalence. -/
+@[simps]
+def pi (E : ∀ i, C i ≌ D i) : (∀ i, C i) ≌ (∀ i, D i) where
+  functor := Functor.pi (fun i => (E i).functor)
+  inverse := Functor.pi (fun i => (E i).inverse)
+  unitIso := NatIso.pi (fun i => (E i).unitIso)
+  counitIso := NatIso.pi (fun i => (E i).counitIso)
+
+instance (F : ∀ i, C i ⥤ D i) [∀ i, IsEquivalence (F i)] :
+    IsEquivalence (Functor.pi F) :=
+  IsEquivalence.ofEquivalence (pi (fun i => (F i).asEquivalence))
+
+end Equivalence
+
 end CategoryTheory

From daf42ee4d7e21235792a22d5bbca3b99dfebc027 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 7 Dec 2023 11:05:36 +0100
Subject: [PATCH 3/6] split PR

---
 Mathlib.lean                                |  1 -
 Mathlib/CategoryTheory/Localization/Pi.lean | 78 ---------------------
 2 files changed, 79 deletions(-)
 delete mode 100644 Mathlib/CategoryTheory/Localization/Pi.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 5fe3355e0b8ef..509febe15a0df 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1135,7 +1135,6 @@ import Mathlib.CategoryTheory.Localization.Construction
 import Mathlib.CategoryTheory.Localization.Equivalence
 import Mathlib.CategoryTheory.Localization.LocalizerMorphism
 import Mathlib.CategoryTheory.Localization.Opposite
-import Mathlib.CategoryTheory.Localization.Pi
 import Mathlib.CategoryTheory.Localization.Predicate
 import Mathlib.CategoryTheory.Localization.Prod
 import Mathlib.CategoryTheory.Monad.Adjunction
diff --git a/Mathlib/CategoryTheory/Localization/Pi.lean b/Mathlib/CategoryTheory/Localization/Pi.lean
deleted file mode 100644
index 4cd04799b021f..0000000000000
--- a/Mathlib/CategoryTheory/Localization/Pi.lean
+++ /dev/null
@@ -1,78 +0,0 @@
-/-
-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
-
-/-!
-# Localization of product categories
-
-In this file, it is shown that if for all `j : J` (with `J` finite),
-functors `L j : C j ⥤ D j` are localization functors with respect
-to a class of morphism `W j : MorphismProperty (C j)`, then the product
-functor `Functor.pi L : (∀ j, C j) ⥤ ∀ j, D j` is a localization
-functor for the product class of morphism `MorphismProperty.pi W`.
-The proof proceeds by induction on the cardinal of `J` using the
-main result of the file `Mathlib.CategoryTheory.Localization.Prod`.
-
--/
-
-universe w v₁ v₂ u₁ u₂
-
-namespace CategoryTheory.Functor.IsLocalization
-
-instance pi {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂}
-  [∀ j, Category.{v₁} (C j)] [∀ j, Category.{v₂} (D j)]
-  (L : ∀ j, C j ⥤ D j) (W : ∀ j, MorphismProperty (C j))
-  [∀ j, (W j).ContainsIdentities] [∀ j, (L j).IsLocalization (W j)] :
-    (Functor.pi L).IsLocalization (MorphismProperty.pi W) := by
-  revert J
-  apply Finite.induction_empty_option
-  · intro J₁ J₂ e hJ₁ C₂ D₂ _ _ L₂ W₂ _ _
-    let C₁ := fun j => (C₂ (e j))
-    let D₁ := fun j => (D₂ (e j))
-    let L₁ : ∀ j, C₁ j ⥤ D₁ j := fun j => (L₂ (e j))
-    let W₁ : ∀ j, MorphismProperty (C₁ j) := fun j => (W₂ (e j))
-    replace hJ₁ := hJ₁ L₁ W₁
-    let E := Pi.equivalenceOfEquiv C₂ e
-    let E' := Pi.equivalenceOfEquiv D₂ e
-    haveI : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor :=
-      (CatCommSq.hInvEquiv E (Functor.pi L₁) (Functor.pi L₂) E').symm ⟨Iso.refl _⟩
-    refine IsLocalization.of_equivalences (Functor.pi L₁)
-      (MorphismProperty.pi W₁) (Functor.pi L₂) (MorphismProperty.pi W₂) E E' ?_
-      (MorphismProperty.IsInvertedBy.pi _ _ (fun _ => Localization.inverts _ _))
-    intro _ _ f hf
-    refine ⟨_, _, E.functor.map f, fun i => ?_, ⟨Iso.refl _⟩⟩
-    have H : ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y) (_ : W₂ j g),
-        W₂ j' ((Pi.eqToEquivalence C₂ h).functor.map g) := by
-      rintro j _ rfl _ _ g hg
-      exact hg
-    exact H (e.apply_symm_apply i) _ (hf (e.symm i))
-  · intro C D _ _ L W _ _
-    haveI : ∀ j, IsEquivalence (L j) := by rintro ⟨⟩
-    refine IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)
-    rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]
-    rintro ⟨⟩
-  · intro J _ hJ C D _ _ L W _ _
-    let C' := fun j => C (some j)
-    let D' := fun j => D (some j)
-    let L' : ∀ j, C' j ⥤ D' j := fun j => L (some j)
-    let W' : ∀ j, MorphismProperty (C' j) := fun j => W (some j)
-    replace hJ := hJ L' W'
-    let L₁ := (L none).prod (Functor.pi L')
-    let L₂ := Functor.pi L
-    haveI : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ L₂
-      (Pi.optionEquivalence D).symm.functor :=
-        ⟨NatIso.pi' (by rintro (_|i) <;> apply Iso.refl)⟩
-    refine IsLocalization.of_equivalences L₁ ((W none).prod (MorphismProperty.pi W')) L₂ _
-      (Pi.optionEquivalence C).symm (Pi.optionEquivalence D).symm ?_ ?_
-    · intro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ f ⟨hf₁, hf₂⟩
-      refine ⟨_, _, (Pi.optionEquivalence C).inverse.map f, ?_, ⟨Iso.refl _⟩⟩
-      · rintro (_|i)
-        · exact hf₁
-        · apply hf₂
-    · apply MorphismProperty.IsInvertedBy.pi
-      rintro (_|i) <;> apply Localization.inverts
-
-end CategoryTheory.Functor.IsLocalization

From d526935a8e496832cb6c1a689835d3f63fd3384c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 7 Dec 2023 11:09:46 +0100
Subject: [PATCH 4/6] removed irrelevant lemma

---
 Mathlib/CategoryTheory/Localization/Predicate.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean
index bde3a8e3310a1..a059c145afd76 100644
--- a/Mathlib/CategoryTheory/Localization/Predicate.lean
+++ b/Mathlib/CategoryTheory/Localization/Predicate.lean
@@ -434,12 +434,6 @@ theorem of_equivalence_target {E : Type*} [Category E] (L' : C ⥤ E) (eq : D 
       nonempty_isEquivalence := Nonempty.intro (IsEquivalence.ofIso e' inferInstance) }
 #align category_theory.functor.is_localization.of_equivalence_target CategoryTheory.Functor.IsLocalization.of_equivalence_target
 
-lemma of_isEquivalence (L : C ⥤ D) (W : MorphismProperty C)
-    (hW : W ⊆ MorphismProperty.isomorphisms C) [IsEquivalence L] :
-    L.IsLocalization W := by
-  haveI : (𝟭 C).IsLocalization W := for_id W hW
-  exact of_equivalence_target (𝟭 C) W L L.asEquivalence L.leftUnitor
-
 end IsLocalization
 
 end Functor

From c83c3f10e6ad9f48ffa97df3aacb3d098cc3edaa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 7 Dec 2023 11:11:49 +0100
Subject: [PATCH 5/6] fixed attribute

---
 Mathlib/CategoryTheory/Pi/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index d03c834aa6798..ab75cc554c327 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -365,7 +365,7 @@ noncomputable def Pi.equivalenceOfEquiv (e : J ≃ I) :
     (Functor.leftUnitor _).symm)
 
 /-- A product of categories indexed by `Option J` identifies to a binary product. -/
-@[simps!]
+@[simps]
 def Pi.optionEquivalence (C' : Option J → Type u₁) [∀ i, Category.{v₁} (C' i)] :
     (∀ i, C' i) ≌ C' none × (∀ (j : J), C' (some j)) where
   functor := Functor.prod' (Pi.eval C' none)

From 3f76245883c069dce7fb94054086d44b3429b97a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 7 Dec 2023 11:12:53 +0100
Subject: [PATCH 6/6] fixed docstring

---
 Mathlib/CategoryTheory/Pi/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index ab75cc554c327..5fae1ca167314 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -383,7 +383,7 @@ namespace Equivalence
 variable {C}
 variable {D : I → Type u₂} [∀ i, Category.{v₂} (D i)]
 
-/-- Assemble an `I`-indexed family of equivalences of categories isomorphisms
+/-- Assemble an `I`-indexed family of equivalences of categories
 into a single equivalence. -/
 @[simps]
 def pi (E : ∀ i, C i ≌ D i) : (∀ i, C i) ≌ (∀ i, D i) where