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)
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯