Lifting of trifunctors

In this file, in the context of the localization of categories, we extend the notion of lifting of functors to the case of trifunctors (see also the file Localization.Bifunctor for the case of bifunctors). The main result in this file is that we can localize "associator" isomorphisms (see the definition Localization.associator).

def CategoryTheory.MorphismProperty.IsInvertedBy₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_13} E] (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (F : Functor C₁ (Functor C₂ (Functor C₃ E))) : Prop

Classes of morphisms W₁ : MorphismProperty C₁, W₂ : MorphismProperty C₂ and W₃ : MorphismProperty C₃ are said to be inverted by F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E if W₁.prod (W₂.prod W₃) is inverted by the functor currying₃.functor.obj F : C₁ × C₂ × C₃ ⥤ E.

Equations

• W₁.IsInvertedBy₃ W₂ W₃ F = (W₁.prod (W₂.prod W₃)).IsInvertedBy (CategoryTheory.currying₃.functor.obj F)

class CategoryTheory.Localization.Lifting₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (F' : Functor D₁ (Functor D₂ (Functor D₃ E))) : Type (max (max (max u_1 u_2) u_20) u_3)

Given functors L₁ : C₁ ⥤ D₁, L₂ : C₂ ⥤ D₂, L₃ : C₃ ⥤ D₃, morphisms properties W₁ on C₁, W₂ on C₂, W₃ on C₃, and functors F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E and F' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E, we say Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F' holds if F is induced by F', up to an isomorphism.

• iso' : ((((whiskeringLeft₃ E).obj L₁).obj L₂).obj L₃).obj F' ≅ F

  the isomorphism ((((whiskeringLeft₃ E).obj L₁).obj L₂).obj L₃).obj F' ≅ F expressing that F is induced by F' up to an isomorphism

noncomputable def CategoryTheory.Localization.Lifting₃.iso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (F' : Functor D₁ (Functor D₂ (Functor D₃ E))) [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F'] : ((((whiskeringLeft₃ E).obj L₁).obj L₂).obj L₃).obj F' ≅ F

The isomorphism ((((whiskeringLeft₃ E).obj L₁).obj L₂).obj L₃).obj F' ≅ F when Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F' holds.

Equations

• CategoryTheory.Localization.Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F F' = CategoryTheory.Localization.Lifting₃.iso' W₁ W₂ W₃

noncomputable instance CategoryTheory.Localization.Lifting₃.uncurry {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (F' : Functor D₁ (Functor D₂ (Functor D₃ E))) [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F'] : Lifting (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F) (uncurry₃.obj F')

Equations

• CategoryTheory.Localization.Lifting₃.uncurry L₁ L₂ L₃ W₁ W₂ W₃ F F' = { iso' := CategoryTheory.uncurry₃.mapIso (CategoryTheory.Localization.Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F F') }

noncomputable def CategoryTheory.Localization.lift₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (hF : W₁.IsInvertedBy₃ W₂ W₃ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] : Functor D₁ (Functor D₂ (Functor D₃ E))

Given localization functor L₁ : C₁ ⥤ D₁, L₂ : C₂ ⥤ D₂ and L₃ : C₃ ⥤ D₃ with respect to W₁ : MorphismProperty C₁, W₂ : MorphismProperty C₂ and W₃ : MorphismProperty C₃ respectively, and a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E which inverts W₁, W₂ and W₃, this is the induced localized trifunctor D₁ ⥤ D₂ ⥤ D₃ ⥤ E.

Equations

• CategoryTheory.Localization.lift₃ F hF L₁ L₂ L₃ = CategoryTheory.curry₃.obj (CategoryTheory.Localization.lift (CategoryTheory.uncurry₃.obj F) hF (L₁.prod (L₂.prod L₃)))

noncomputable instance CategoryTheory.Localization.instLifting₃Lift₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (hF : W₁.IsInvertedBy₃ W₂ W₃ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F (lift₃ F hF L₁ L₂ L₃)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Localization.lift₃NatTrans {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ E))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ E))) [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'] [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (τ : F₁ ⟶ F₂) : F₁' ⟶ F₂'

The natural transformation F₁' ⟶ F₂' of trifunctors induced by a natural transformation τ : F₁ ⟶ F₂ when Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁' and Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂' hold.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Localization.lift₃NatTrans_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_18, u_1} C₁] [Category.{u_19, u_2} C₂] [Category.{u_20, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_16, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_14, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ E))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ E))) [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'] [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) = CategoryStruct.comp ((((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃) (CategoryStruct.comp (((τ.app X₁).app X₂).app X₃) ((((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃))

theorem CategoryTheory.Localization.natTrans₃_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_18, u_1} C₁] [Category.{u_19, u_2} C₂] [Category.{u_20, u_3} C₃] [Category.{u_15, u_6} D₁] [Category.{u_16, u_7} D₂] [Category.{u_17, u_8} D₃] [Category.{u_14, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] {F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ E))} {τ τ' : F₁' ⟶ F₂'} (h : ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃), ((τ.app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) = ((τ'.app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃)) : τ = τ'

noncomputable def CategoryTheory.Localization.lift₃NatIso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ E))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ E))) [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'] [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (e : F₁ ≅ F₂) : F₁' ≅ F₂'

The natural isomorphism F₁' ≅ F₂' of trifunctors induced by a natural isomorphism e : F₁ ≅ F₂ when Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁' and Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂' hold.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Localization.lift₃NatIso_inv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ E))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ E))) [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'] [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (e : F₁ ≅ F₂) : (lift₃NatIso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e).inv = lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₁ F₂' F₁' e.inv

@[simp]

theorem CategoryTheory.Localization.lift₃NatIso_hom {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_13} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_13} E] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ E))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ E))) [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'] [Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'] (e : F₁ ≅ F₂) : (lift₃NatIso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e).hom = lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e.hom

noncomputable def CategoryTheory.Localization.Lifting₃.bifunctorComp₁₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₁₂ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {D₁₂ : Type u_9} {C : Type u_11} {D : Type u_12} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_4} C₁₂] [Category.{u_21, u_9} D₁₂] [Category.{u_22, u_11} C] [Category.{u_23, u_12} D] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (L₁₂ : Functor C₁₂ D₁₂) (L : Functor C D) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (W₁₂ : MorphismProperty C₁₂) (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C)) (F₁₂' : Functor D₁ (Functor D₂ D₁₂)) (G' : Functor D₁₂ (Functor D₃ D)) [Lifting₂ L₁ L₂ W₁ W₂ (F₁₂.comp ((whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂)) F₁₂'] [Lifting₂ L₁₂ L₃ W₁₂ W₃ (G.comp ((whiskeringRight C₃ C D).obj L)) G'] : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ ((Functor.postcompose₃.obj L).obj (CategoryTheory.bifunctorComp₁₂ F₁₂ G)) (CategoryTheory.bifunctorComp₁₂ F₁₂' G')

The construction bifunctorComp₁₂ of a trifunctor by composition of bifunctors is compatible with localization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Localization.Lifting₃.bifunctorComp₂₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₂₃ : Type u_5} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {D₂₃ : Type u_10} {C : Type u_11} {D : Type u_12} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_5} C₂₃] [Category.{u_21, u_10} D₂₃] [Category.{u_22, u_11} C] [Category.{u_23, u_12} D] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (L₂₃ : Functor C₂₃ D₂₃) (L : Functor C D) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (W₂₃ : MorphismProperty C₂₃) (F : Functor C₁ (Functor C₂₃ C)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (F' : Functor D₁ (Functor D₂₃ D)) (G₂₃' : Functor D₂ (Functor D₃ D₂₃)) [Lifting₂ L₁ L₂₃ W₁ W₂₃ (F.comp ((whiskeringRight C₂₃ C D).obj L)) F'] [Lifting₂ L₂ L₃ W₂ W₃ (G₂₃.comp ((whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃)) G₂₃'] : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ ((Functor.postcompose₃.obj L).obj (CategoryTheory.bifunctorComp₂₃ F G₂₃)) (CategoryTheory.bifunctorComp₂₃ F' G₂₃')

The construction bifunctorComp₂₃ of a trifunctor by composition of bifunctors is compatible with localization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def 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} [Category.{u_14, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_16, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_18, u_7} D₂] [Category.{u_19, u_8} D₃] [Category.{u_20, u_4} C₁₂] [Category.{u_21, u_5} C₂₃] [Category.{u_22, u_9} D₁₂] [Category.{u_23, u_10} D₂₃] [Category.{u_24, u_11} C] [Category.{u_25, u_12} D] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (L₁₂ : Functor C₁₂ D₁₂) (L₂₃ : Functor C₂₃ D₂₃) (L : Functor C D) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (W₁₂ : MorphismProperty C₁₂) (W₂₃ : MorphismProperty C₂₃) [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] {F₁₂ : Functor C₁ (Functor C₂ C₁₂)} {G : Functor C₁₂ (Functor C₃ C)} {F : Functor C₁ (Functor C₂₃ C)} {G₂₃ : Functor C₂ (Functor C₃ C₂₃)} (iso : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃) (F₁₂' : Functor D₁ (Functor D₂ D₁₂)) (G' : Functor D₁₂ (Functor D₃ D)) (F' : Functor D₁ (Functor D₂₃ D)) (G₂₃' : Functor D₂ (Functor D₃ D₂₃)) [Lifting₂ L₁ L₂ W₁ W₂ (F₁₂.comp ((whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂)) F₁₂'] [Lifting₂ L₁₂ L₃ W₁₂ W₃ (G.comp ((whiskeringRight C₃ C D).obj L)) G'] [Lifting₂ L₁ L₂₃ W₁ W₂₃ (F.comp ((whiskeringRight C₂₃ C D).obj L)) F'] [Lifting₂ L₂ L₃ W₂ W₃ (G₂₃.comp ((whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃)) G₂₃'] : bifunctorComp₁₂ F₁₂' G' ≅ bifunctorComp₂₃ F' G₂₃'

The associator isomorphism obtained by localization.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Localization.associator_hom_app_app_app {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} [Category.{u_19, u_1} C₁] [Category.{u_20, u_2} C₂] [Category.{u_21, u_3} C₃] [Category.{u_17, u_6} D₁] [Category.{u_16, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_23, u_4} C₁₂] [Category.{u_24, u_5} C₂₃] [Category.{u_18, u_9} D₁₂] [Category.{u_22, u_10} D₂₃] [Category.{u_25, u_11} C] [Category.{u_14, u_12} D] (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (L₁₂ : Functor C₁₂ D₁₂) (L₂₃ : Functor C₂₃ D₂₃) (L : Functor C D) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (W₁₂ : MorphismProperty C₁₂) (W₂₃ : MorphismProperty C₂₃) [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] {F₁₂ : Functor C₁ (Functor C₂ C₁₂)} {G : Functor C₁₂ (Functor C₃ C)} {F : Functor C₁ (Functor C₂₃ C)} {G₂₃ : Functor C₂ (Functor C₃ C₂₃)} (iso : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃) (F₁₂' : Functor D₁ (Functor D₂ D₁₂)) (G' : Functor D₁₂ (Functor D₃ D)) (F' : Functor D₁ (Functor D₂₃ D)) (G₂₃' : Functor D₂ (Functor D₃ D₂₃)) [Lifting₂ L₁ L₂ W₁ W₂ (F₁₂.comp ((whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂)) F₁₂'] [Lifting₂ L₁₂ L₃ W₁₂ W₃ (G.comp ((whiskeringRight C₃ C D).obj L)) G'] [Lifting₂ L₁ L₂₃ W₁ W₂₃ (F.comp ((whiskeringRight C₂₃ C D).obj L)) F'] [Lifting₂ L₂ L₃ W₂ W₃ (G₂₃.comp ((whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃)) G₂₃'] (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((associator L₁ L₂ L₃ L₁₂ L₂₃ L W₁ W₂ W₃ W₁₂ W₂₃ iso F₁₂' G' F' G₂₃').hom.app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) = CategoryStruct.comp ((G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂.comp ((whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂)) F₁₂').hom.app X₁).app X₂)).app (L₃.obj X₃)) (CategoryStruct.comp (((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G.comp ((whiskeringRight C₃ C D).obj L)) G').hom.app ((F₁₂.obj X₁).obj X₂)).app X₃) (CategoryStruct.comp (L.map (((iso.hom.app X₁).app X₂).app X₃)) (CategoryStruct.comp (((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F.comp ((whiskeringRight C₂₃ C D).obj L)) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃)) ((F'.obj (L₁.obj X₁)).map (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃.comp ((whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃)) G₂₃').inv.app X₂).app X₃)))))