Lift of a "single functor" to a full subcategory

Let C, D and E be categories. Let A be an additive monoid. Assume that D and E have shifts by A and that we have a fully faithful functor G : D ⥤ A which commutes with shifts. Given F : SingleFunctors C E A, and a family of functors Φ a : C ⥤ D with isomorphisms Φ a ⋙ G ≅ F.functor a for all a : A, we lift F in SingleFunctor C D A.

@[irreducible]

noncomputable def CategoryTheory.SingleFunctors.lift.shiftIso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] {F : SingleFunctors C E A} {G : Functor D E} [G.CommShift A] [G.Full] [G.Faithful] {Φ : A → Functor C D} (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (n a a' : A) (h : n + a = a') : (Φ a').comp (shiftFunctor D n) ≅ Φ a

Auxiliary definition for SingleFunctors.lift.

Equations

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

noncomputable def CategoryTheory.SingleFunctors.lift {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) : SingleFunctors C D A

Let C, D and E be categories. Let A be an additive monoid. Assume that D and E have shifts by A and that we have a fully faithful functor G : D ⥤ A which commutes with shifts. Given F : SingleFunctors C E A, and a family of functors Φ a : C ⥤ D with isomorphisms Φ a ⋙ G ≅ F.functor a for all a : A, this is a term in SingleFunctors C D A which is given by the functors Φ a for all a.

Equations

• F.lift G Φ hΦ = { functor := Φ, shiftIso := CategoryTheory.SingleFunctors.lift.shiftIso hΦ, shiftIso_zero := ⋯, shiftIso_add := ⋯ }

@[simp]

theorem CategoryTheory.SingleFunctors.lift_functor {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (a✝ : A) : (F.lift G Φ hΦ).functor a✝ = Φ a✝

theorem CategoryTheory.SingleFunctors.map_lift_shiftIso_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (n a a' : A) (h : n + a = a') (X : C) : G.map (((F.lift G Φ hΦ).shiftIso n a a' h).hom.app X) = CategoryStruct.comp ((Functor.commShiftIso G n).hom.app ((Φ a').obj X)) (CategoryStruct.comp ((shiftFunctor E n).map ((hΦ a').hom.app X)) (CategoryStruct.comp ((F.shiftIso n a a' h).hom.app X) ((hΦ a).inv.app X)))

theorem CategoryTheory.SingleFunctors.map_lift_shiftIso_hom_app_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (n a a' : A) (h : n + a = a') (X : C) {Z : E} (h✝ : G.obj ((Φ a).obj X) ⟶ Z) : CategoryStruct.comp (G.map (((F.lift G Φ hΦ).shiftIso n a a' h).hom.app X)) h✝ = CategoryStruct.comp ((Functor.commShiftIso G n).hom.app ((Φ a').obj X)) (CategoryStruct.comp ((shiftFunctor E n).map ((hΦ a').hom.app X)) (CategoryStruct.comp ((F.shiftIso n a a' h).hom.app X) (CategoryStruct.comp ((hΦ a).inv.app X) h✝)))

noncomputable def CategoryTheory.SingleFunctors.liftPostcompIso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) : (F.lift G Φ hΦ).postcomp G ≅ F

After postcomposition with the fully faithful functor G, lift F G Φ hΦ becomes isomorphic to F.

Equations

• F.liftPostcompIso G Φ hΦ = CategoryTheory.SingleFunctors.isoMk hΦ ⋯

@[simp]

theorem CategoryTheory.SingleFunctors.liftPostcompIso_inv_hom {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (a : A) : (F.liftPostcompIso G Φ hΦ).inv.hom a = (hΦ a).inv

@[simp]

theorem CategoryTheory.SingleFunctors.liftPostcompIso_hom_hom {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (a : A) : (F.liftPostcompIso G Φ hΦ).hom.hom a = (hΦ a).hom

instance CategoryTheory.SingleFunctors.instAdditiveFunctorLift {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] [Category.{u_7, u_3} E] {A : Type u_4} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C E A) (G : Functor D E) [G.CommShift A] [G.Full] [G.Faithful] (Φ : A → Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) [Preadditive C] [Preadditive D] [Preadditive E] [G.Additive] (a : A) [(F.functor a).Additive] : ((F.lift G Φ hΦ).functor a).Additive