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.lean.
instance CategoryTheory.Functor.IsLocalization.pi {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [(j : J) → Category.{v₁, u₁} (C j)] [(j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor (C j) (D j)) (W : (j : J) → MorphismProperty (C j)) [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)] :
instance CategoryTheory.Functor.IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities {J : Type} [Finite J] {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [W.ContainsIdentities] [L.IsLocalization W] :
((whiskeringRight (Discrete J) C D).obj L).IsLocalization (W.functorCategory (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.