Lifting of quadrifunctors

In this file, in the context of the localization of categories, we extend the notion of lifting of functors to the case of quadrifunctors. The definitions reduce to functors on the right-associated product category by currying and uncurrying.

def CategoryTheory.MorphismProperty.IsInvertedBy₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_9, u_9} E] (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃) (W₄ : MorphismProperty C₄) (F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) : Prop

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

Equations

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

class CategoryTheory.Localization.Lifting₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₂ (Functor C₃ (Functor C₄ E)))) (F' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))) : Type (max (max (max (max u_1 u_2) u_3) u_4) v_9)

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

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

  The isomorphism expressing that F is induced by F', up to an isomorphism.

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.Lifting₄.uncurry {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₂ (Functor C₃ (Functor C₄ E)))) (F' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))) [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F F'] : Lifting (L₁.prod (L₂.prod (L₃.prod L₄))) (W₁.prod (W₂.prod (W₃.prod W₄))) (Functor.uncurry₄.obj F) (Functor.uncurry₄.obj F')

Equations

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

@[implicit_reducible]

noncomputable def CategoryTheory.Localization.lift₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} {W₄ : MorphismProperty C₄} (hF : W₁.IsInvertedBy₄ W₂ W₃ W₄ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (L₄ : Functor C₄ D₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))

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

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.instLifting₄Lift₄ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} {W₄ : MorphismProperty C₄} (hF : W₁.IsInvertedBy₄ W₂ W₃ W₄ F) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (L₄ : Functor C₄ D₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] : Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F (lift₄ F hF L₁ L₂ L₃ L₄)

Equations

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

@[implicit_reducible]

noncomputable def CategoryTheory.Localization.lift₄NatTrans {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))) [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₁'] [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₂ F₂'] (τ : F₁ ⟶ F₂) : F₁' ⟶ F₂'

The natural transformation F₁' ⟶ F₂' of quadrifunctors induced by a natural transformation τ : F₁ ⟶ F₂ when F₁' and F₂' lift F₁ and F₂, respectively.

Equations

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

@[simp]

theorem CategoryTheory.Localization.lift₄NatTrans_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))) [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₁'] [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₂ F₂'] (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) (X₄ : C₄) : ((((lift₄NatTrans L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃)).app (L₄.obj X₄) = CategoryStruct.comp (((((Lifting₄.iso L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₁').hom.app X₁).app X₂).app X₃).app X₄) (CategoryStruct.comp ((((τ.app X₁).app X₂).app X₃).app X₄) (((((Lifting₄.iso L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₂ F₂').inv.app X₁).app X₂).app X₃).app X₄))

theorem CategoryTheory.Localization.natTrans₄_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] {F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))} {τ τ' : F₁' ⟶ F₂'} (h : ∀ (X₁ : C₁) (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₂)).app (L₃.obj X₃)).app (L₄.obj X₄)) : τ = τ'

Two natural transformations between quadrifunctors on localized categories are equal if their components agree on objects in the images of the four localization functors.

@[implicit_reducible]

noncomputable def CategoryTheory.Localization.lift₄NatIso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))) [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₁'] [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₂ F₂'] (e : F₁ ≅ F₂) : F₁' ≅ F₂'

The natural isomorphism F₁' ≅ F₂' of quadrifunctors induced by a natural isomorphism e : F₁ ≅ F₂ when F₁' and F₂' lift F₁ and F₂, respectively.

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} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))) [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₁'] [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₂ F₂'] (e : F₁ ≅ F₂) : (lift₄NatIso L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₂ F₁' F₂' e).inv = lift₄NatTrans L₁ L₂ L₃ L₄ W₁ 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} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} {E : Type u_9} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] [Category.{v_9, u_9} E] (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₄) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [L₃.IsLocalization W₃] [L₄.IsLocalization W₄] [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₃.ContainsIdentities] [W₄.ContainsIdentities] (F₁ F₂ : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))) (F₁' F₂' : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))) [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₁'] [Lifting₄ L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₂ F₂'] (e : F₁ ≅ F₂) : (lift₄NatIso L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₂ F₁' F₂' e).hom = lift₄NatTrans L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄ F₁ F₂ F₁' F₂' e.hom