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

Auxiliary definition for prodLift.

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

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

        Equations
        • =