Theorems · Theorem · category theory

CategoryTheory.Localization.associator.congr_simp

∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₁₂ : Type u_4} {C₂₃ : Type u_5} {D₁ : Type u_6} {D₂ : Type u_7}
  {D₃ : Type u_8} {D₁₂ : Type u_9} {D₂₃ : Type u_10} {C : Type u_11} {D : Type u_12}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_7, u_4} C₁₂] [inst_7 : CategoryTheory.Category.{v_8, u_5} C₂₃]
  [inst_8 : CategoryTheory.Category.{v_9, u_9} D₁₂] [inst_9 : CategoryTheory.Category.{v_10, u_10} D₂₃]
  [inst_10 : CategoryTheory.Category.{v_11, u_11} C] [inst_11 : CategoryTheory.Category.{v_12, u_12} D]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃)
  (L₁₂ : CategoryTheory.Functor C₁₂ D₁₂) (L₂₃ : CategoryTheory.Functor C₂₃ D₂₃) (L : CategoryTheory.Functor C D)
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂)
  (W₃ : CategoryTheory.MorphismProperty C₃) (W₁₂ : CategoryTheory.MorphismProperty C₁₂)
  (W₂₃ : CategoryTheory.MorphismProperty C₂₃) [inst_12 : W₁.ContainsIdentities] [inst_13 : W₂.ContainsIdentities]
  [inst_14 : W₃.ContainsIdentities] [inst_15 : L₁.IsLocalization W₁] [inst_16 : L₂.IsLocalization W₂]
  [inst_17 : L₃.IsLocalization W₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (iso iso_1 : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃),
  iso = iso_1 →
    ∀ (F₁₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ D₁₂))
      (G' : CategoryTheory.Functor D₁₂ (CategoryTheory.Functor D₃ D))
      (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂₃ D))
      (G₂₃' : CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ D₂₃)), ⋯

Defined in

Mathlib.CategoryTheory.Localization.Monoidal.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MorphismProperty.ContainsIdentitiesCategoryTheory.MorphismProperty.ContainsIdentitiesCategoryTheory.MorphismProperty.ContainsIdentitiesCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.Localization.Lifting₂CategoryTheory.Localization.Lifting₂CategoryTheory.Localization.Lifting₂CategoryTheory.Localization.Lifting₂