Theorems · Definition · category theory

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        (W₁ : CategoryTheory.MorphismProperty C₁) →
          (W₂ : CategoryTheory.MorphismProperty C₂) →
            {E : Type u₅} →
              [inst_2 : CategoryTheory.Category.{v₅, u₅} E] →
                [W₁.ContainsIdentities] →
                  [W₂.ContainsIdentities] →
                    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.

Defined in

Mathlib.CategoryTheory.Localization.Prod

Cited by

1 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MorphismProperty.ContainsIdentitiesCategoryTheory.MorphismProperty.ContainsIdentities