Lifting bifunctors to full subcategories

If a bifunctor preserves an object property in two inputs satisfying that property, it restricts to the corresponding full subcategory in both variables. The construction below is the two-variable analogue of Mathlib's ObjectProperty.lift.

Main results

CategoryTheory.ObjectProperty.lift₂CommShift₂Int transports the ambient CommShift₂Int structure, including its Koszul compatibility, through lift₂ when the property is shift-stable. It returns explicit data rather than a global instance, avoiding instance diamonds between independent restrictions.

def CategoryTheory.ObjectProperty.lift₂ {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (F : Functor C (Functor C C)) (hF : ∀ (X Y : C), P X → P Y → P ((F.obj X).obj Y)) : Functor P.FullSubcategory (Functor P.FullSubcategory P.FullSubcategory)

Restrict a bifunctor to a full subcategory when it preserves the defining property in both variables.

Equations

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

@[simp]

theorem CategoryTheory.ObjectProperty.lift₂_map_app {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (F : Functor C (Functor C C)) (hF : ∀ (X Y : C), P X → P Y → P ((F.obj X).obj Y)) {X Y : P.FullSubcategory} (f : X ⟶ Y) (Z : P.FullSubcategory) : ((P.lift₂ F hF).map f).app Z = homMk ((F.map f.hom).app Z.obj)

@[simp]

theorem CategoryTheory.ObjectProperty.lift₂_obj {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (F : Functor C (Functor C C)) (hF : ∀ (X Y : C), P X → P Y → P ((F.obj X).obj Y)) (X : P.FullSubcategory) : (P.lift₂ F hF).obj X = P.lift (P.ι.comp (F.obj X.obj)) ⋯

def CategoryTheory.ObjectProperty.lift₂CompιIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (F : Functor C (Functor C C)) (hF : ∀ (X Y : C), P X → P Y → P ((F.obj X).obj Y)) : (P.lift₂ F hF).comp ((Functor.whiskeringRight P.FullSubcategory P.FullSubcategory C).obj P.ι) ≅ P.ι.comp (F.comp ((Functor.whiskeringLeft P.FullSubcategory C C).obj P.ι))

Forgetting the output of lift₂ recovers the original bifunctor restricted along the inclusion in both inputs. This is definitionally an identity isomorphism.

Equations

• P.lift₂CompιIso F hF = CategoryTheory.Iso.refl ((P.lift₂ F hF).comp ((CategoryTheory.Functor.whiskeringRight P.FullSubcategory P.FullSubcategory C).obj P.ι))

@[reducible]

noncomputable def CategoryTheory.ObjectProperty.lift₂CommShift₂Int {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [P.IsStableUnderShift ℤ] (F : Functor C (Functor C C)) [F.CommShift₂Int] (hF : ∀ (X Y : C), P X → P Y → P ((F.obj X).obj Y)) : (P.lift₂ F hF).CommShift₂Int

A coherent shift package for the restriction of a bifunctor to a shift-stable full subcategory. This is explicit data, rather than a global instance, so independent restricted bifunctors do not create an instance diamond.

Equations

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

theorem CategoryTheory.ObjectProperty.maps₂_of_comp_of_essSurj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) [P.IsClosedUnderIsomorphisms] (L : Functor C D) [L.EssSurj] (F : Functor D (Functor D D)) (G : Functor C (Functor C D)) (e : (((Functor.whiskeringLeft₂ D).obj L).obj L).obj F ≅ G) (hG : ∀ (X Y : C), P (L.obj X) → P (L.obj Y) → P ((G.obj X).obj Y)) (X Y : D) : P X → P Y → P ((F.obj X).obj Y)

To prove that a bifunctor preserves an isomorphism-stable object property, it suffices to check the claim after presenting both inputs through an essentially surjective functor.