Theorems · Definition · category theory

CategoryTheory.Localization.associator

{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₂₃) →
                                                                      [W₁.ContainsIdentities] →
                                                                        [W₂.ContainsIdentities] →
                                                                          [W₃.ContainsIdentities] →
                                                                            [L₁.IsLocalization W₁] →
                                                                              [L₂.IsLocalization W₂] →
                                                                                [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₂₃)} →
                                                                                          (CategoryTheory.bifunctorComp₁₂
                                                                                                F₁₂ G ≅
                                                                                              CategoryTheory.bifunctorComp₂₃
                                                                                                F G₂₃) →
                                                                                            (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₂₃)) →
                                                                                                    [⋯] → ⋯

The associator isomorphism obtained by localization.

Defined in: Mathlib.CategoryTheory.Localization.Trifunctor
Cited by: 3 results in Mathlib
Foundations: Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.MorphismProperty.ContainsIdentities CategoryTheory.MorphismProperty.ContainsIdentities CategoryTheory.MorphismProperty.ContainsIdentities CategoryTheory.Functor.IsLocalization CategoryTheory.Functor.IsLocalization CategoryTheory.Functor.IsLocalization CategoryTheory.Localization.Lifting₂ CategoryTheory.Localization.Lifting₂ CategoryTheory.Localization.Lifting₂ CategoryTheory.Localization.Lifting₂

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.Functor.compstatement and proof · cited by 6,529
CategoryTheory.Isostatement and proof · cited by 3,963
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.Functor.IsLocalizationstatement and proof · cited by 432
CategoryTheory.Functor.mapIsoproof · cited by 224
CategoryTheory.Functor.whiskeringRightstatement and proof · cited by 221
CategoryTheory.MorphismProperty.ContainsIdentitiesstatement and proof · cited by 94
CategoryTheory.bifunctorComp₂₃statement and proof · cited by 55
CategoryTheory.bifunctorComp₁₂statement and proof · cited by 53

Cited by4

Results whose statement or proof uses this declaration.

CategoryTheory.Localization.Monoidal.associator_hom_appproof · cited by 2
CategoryTheory.Localization.associator_hom_app_app_appstatement · cited by 1
CategoryTheory.Localization.Monoidal.associatorproof · cited by 1
CategoryTheory.Localization.associator.congr_simpstatement and proof · cited by 0