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

• ⋯ = ⋯