Localization of product categories #
In this file, it is shown that if functors L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂
are localization functors for morphisms properties W₁ and W₂, then
the product functor C₁ × C₂ ⥤ D₁ × D₂ is a localization functor for
W₁.prod W₂ : MorphismProperty (C₁ × C₂), at least if both W₁ and W₂
contain identities. This main result is the instance Functor.IsLocalization.prod.
The proof proceeds by showing first Localization.Construction.prodIsLocalization,
which asserts that this holds for the localization functors W₁.Q and W₂.Q to
the constructed localized categories: this is done by showing that the product
functor W₁.Q.prod W₂.Q : C₁ × C₂ ⥤ W₁.Localization × W₂.Localization satisfies
the strict universal property of the localization for W₁.prod W₂. The general
case follows by transporting this result through equivalences of categories.
noncomputable def
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
(F : CategoryTheory.Functor (C₁ × C₂) E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.prod W₁ W₂) F)
:
Auxiliary definition for prodLift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
(F : CategoryTheory.Functor (C₁ × C₂) E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.prod W₁ W₂) F)
:
CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W₁)
(CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF) = CategoryTheory.curry.toPrefunctor.obj F
noncomputable def
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
[CategoryTheory.MorphismProperty.ContainsIdentities W₁]
{W₂ : CategoryTheory.MorphismProperty C₂}
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
(F : CategoryTheory.Functor (C₁ × C₂) E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.prod W₁ W₂) F)
:
The lifting of a functor F : C₁ × C₂ ⥤ E inverting W₁.prod W₂ to a functor
W₁.Localization × W₂.Localization ⥤ E
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
[CategoryTheory.MorphismProperty.ContainsIdentities W₁]
{W₂ : CategoryTheory.MorphismProperty C₂}
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
(F : CategoryTheory.Functor (C₁ × C₂) E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.prod W₁ W₂) F)
:
CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.Q W₂)
(CategoryTheory.Functor.flip
(CategoryTheory.curry.toPrefunctor.obj
(CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF))) = CategoryTheory.Functor.flip (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF)
theorem
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
[CategoryTheory.MorphismProperty.ContainsIdentities W₁]
{W₂ : CategoryTheory.MorphismProperty C₂}
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
(F : CategoryTheory.Functor (C₁ × C₂) E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.prod W₁ W₂) F)
:
theorem
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_uniq
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
(F₁ : CategoryTheory.Functor
(CategoryTheory.MorphismProperty.Localization W₁ × CategoryTheory.MorphismProperty.Localization W₂) E)
(F₂ : CategoryTheory.Functor
(CategoryTheory.MorphismProperty.Localization W₁ × CategoryTheory.MorphismProperty.Localization W₂) E)
(h : CategoryTheory.Functor.comp
(CategoryTheory.Functor.prod (CategoryTheory.MorphismProperty.Q W₁) (CategoryTheory.MorphismProperty.Q W₂)) F₁ = CategoryTheory.Functor.comp
(CategoryTheory.Functor.prod (CategoryTheory.MorphismProperty.Q W₁) (CategoryTheory.MorphismProperty.Q W₂)) F₂)
:
F₁ = F₂
noncomputable def
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
(W₁ : CategoryTheory.MorphismProperty C₁)
[CategoryTheory.MorphismProperty.ContainsIdentities W₁]
(W₂ : CategoryTheory.MorphismProperty C₂)
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
:
The product of two (constructed) localized categories satisfies the universal property of the localized category of the product.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Localization.Construction.prodIsLocalization
{C₁ : Type u₁}
{C₂ : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
(W₁ : CategoryTheory.MorphismProperty C₁)
[CategoryTheory.MorphismProperty.ContainsIdentities W₁]
(W₂ : CategoryTheory.MorphismProperty C₂)
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
:
instance
CategoryTheory.Functor.IsLocalization.prod
{C₁ : Type u₁}
{C₂ : Type u₂}
{D₁ : Type u₃}
{D₂ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} D₁]
[CategoryTheory.Category.{v₄, u₄} D₂]
(L₁ : CategoryTheory.Functor C₁ D₁)
(W₁ : CategoryTheory.MorphismProperty C₁)
[CategoryTheory.MorphismProperty.ContainsIdentities W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
(W₂ : CategoryTheory.MorphismProperty C₂)
[CategoryTheory.MorphismProperty.ContainsIdentities W₂]
[CategoryTheory.Functor.IsLocalization L₁ W₁]
[CategoryTheory.Functor.IsLocalization L₂ W₂]
:
If L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ are localization functors
for W₁ : MorphismProperty C₁ and W₂ : MorphismProperty C₂ respectively,
and if both W₁ and W₂ contain identites, then the product
functor L₁.prod L₂ : C₁ × C₂ ⥤ D₁ × D₂ is a localization functor for W₁.prod W₂.
Equations
- One or more equations did not get rendered due to their size.