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.

source
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₂
source
noncomputable def CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ {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 : Functor (C₁ × C₂) E) [W₂.ContainsIdentities] (hF : (W₁.prod W₂).IsInvertedBy F) :
Functor W₁.Localization (Functor C₂ E)

Auxiliary definition for prodLift.

Equations
    Instances For
      source
      theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁ {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 : Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [W₂.ContainsIdentities] :
      W₁.Q.comp (prodLift₁ F hF) = Functor.curry.obj F
      source
      noncomputable def CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift {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 : Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [W₁.ContainsIdentities] [W₂.ContainsIdentities] :
      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
        Instances For
          source
          theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂ {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 : Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [W₁.ContainsIdentities] [W₂.ContainsIdentities] :
          W₂.Q.comp (Functor.curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip
          source
          theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac {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 : Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [W₁.ContainsIdentities] [W₂.ContainsIdentities] :
          (W₁.Q.prod W₂.Q).comp (prodLift F hF) = F
          source
          noncomputable def CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod {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] [W₁.ContainsIdentities] [W₂.ContainsIdentities] :
          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
            Instances For
              source
              theorem CategoryTheory.Localization.Construction.prodIsLocalization {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [W₁.ContainsIdentities] [W₂.ContainsIdentities] :
              (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)
              source
              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₂.