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), CategoryTheory.MorphismProperty.ContainsIdentities (W j)]
[∀ (j : J), CategoryTheory.Functor.IsLocalization (L j) (W j)]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.IsLocalization.instIsLocalizationFunctorDiscreteDiscreteCategoryFunctorCategoryCategoryObjFunctorToQuiverToCategoryStructCategoryFunctorToQuiverToCategoryStructCategoryToPrefunctorWhiskeringRightFunctorCategory
{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)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
[CategoryTheory.Functor.IsLocalization L W]
:
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.
Equations
- ⋯ = ⋯