Theorems · Definition · category theory

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift

{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] →
                (F : CategoryTheory.Functor (C₁ × C₂) E) →
                  (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

Defined in

Mathlib.CategoryTheory.Localization.Prod

Cited by

2 results in Mathlib

Foundations

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

Assumes

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