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 morphisms 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 morphisms MorphismProperty.pi W. The proof proceeds by induction on the cardinal of J using the main result of the file Mathlib.CategoryTheory.Localization.Prod.

instance CategoryTheory.Functor.IsLocalization.pi {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [(j : J) → CategoryTheory.Category.{v₁, u₁} (C j)] [(j : J) → CategoryTheory.Category.{v₂, u₂} (D j)] (L : (j : J) → CategoryTheory.Functor (C j) (D j)) (W : (j : J) → CategoryTheory.MorphismProperty (C j)) [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)] : (CategoryTheory.Functor.pi L).IsLocalization (CategoryTheory.MorphismProperty.pi W)

instance CategoryTheory.Functor.IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities {J : Type} [Finite J] {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities] [L.IsLocalization W] : ((CategoryTheory.whiskeringRight (CategoryTheory.Discrete J) C D).obj L).IsLocalization (W.functorCategory (CategoryTheory.Discrete J))

If L : C ⥤ D is a localization functor for W : MorphismProperty C, then the induced functor (Discrete J ⥤ C) ⥤ (Discrete J ⥤ D) is also a localization for W.functorCategory (Discrete J) if W contains identities.