Documentation

Mathlib.CategoryTheory.Localization.Prod

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.

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

    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
      instance CategoryTheory.Functor.IsLocalization.prod {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₃} {D₂ : Type u₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} D₁] [Category.{v₄, u₄} D₂] (L₁ : Functor C₁ D₁) (W₁ : MorphismProperty C₁) (L₂ : Functor C₂ D₂) (W₂ : MorphismProperty C₂) [W₁.ContainsIdentities] [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 identities, then the product functor L₁.prod L₂ : C₁ × C₂ ⥤ D₁ × D₂ is a localization functor for W₁.prod W₂.