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₂} [W₂.ContainsIdentities] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) : CategoryTheory.Functor W₁.Localization (CategoryTheory.Functor C₂ E)

Auxiliary definition for prodLift.

Equations

• CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF = CategoryTheory.Localization.Construction.lift (CategoryTheory.curry.obj F) ⋯

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₂} [W₂.ContainsIdentities] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) : W₁.Q.comp (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF) = CategoryTheory.curry.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₁} [W₁.ContainsIdentities] {W₂ : CategoryTheory.MorphismProperty C₂} [W₂.ContainsIdentities] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) : CategoryTheory.Functor (W₁.Localization × W₂.Localization) E

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.

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₁.ContainsIdentities] {W₂ : CategoryTheory.MorphismProperty C₂} [W₂.ContainsIdentities] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) : W₂.Q.comp (CategoryTheory.curry.obj (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF)).flip = (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF).flip

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₁.ContainsIdentities] {W₂ : CategoryTheory.MorphismProperty C₂} [W₂.ContainsIdentities] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) : (W₁.Q.prod W₂.Q).comp (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF) = 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 (W₁.Localization × W₂.Localization) E) (F₂ : CategoryTheory.Functor (W₁.Localization × W₂.Localization) E) (h : (W₁.Q.prod W₂.Q).comp F₁ = (W₁.Q.prod W₂.Q).comp 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₁) [W₁.ContainsIdentities] (W₂ : CategoryTheory.MorphismProperty C₂) [W₂.ContainsIdentities] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (W₁.Q.prod W₂.Q) (W₁.prod W₂) E

The product of two (constructed) localized categories satisfies the universal property of the localized category of the product.

Equations

• CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod W₁ W₂ = { inverts := ⋯, lift := CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift, fac := ⋯, uniq := ⋯ }

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₁) [W₁.ContainsIdentities] (W₂ : CategoryTheory.MorphismProperty C₂) [W₂.ContainsIdentities] : (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod 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₁) [W₁.ContainsIdentities] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [W₂.ContainsIdentities] [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] : (L₁.prod L₂).IsLocalization (W₁.prod 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

• ⋯ = ⋯