Homological complexes in full subcategories

def HomologicalComplex.liftObjectProperty {ι : Type u_1} {c : ComplexShape ι} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (K : HomologicalComplex V c) (hK : ∀ (n : ι), P (K.X n)) : HomologicalComplex P.FullSubcategory c

Given P : ObjectProperty V and K : HomologicalComplex V c, this is a lift of K in HomologicalComplex P.FullSubcategory c when K.X n satisfies P for all n.

Equations

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

@[simp]

theorem HomologicalComplex.liftObjectProperty_X {ι : Type u_1} {c : ComplexShape ι} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (K : HomologicalComplex V c) (hK : ∀ (n : ι), P (K.X n)) (n : ι) : (liftObjectProperty P K hK).X n = { obj := K.X n, property := ⋯ }

@[simp]

theorem HomologicalComplex.liftObjectProperty_d {ι : Type u_1} {c : ComplexShape ι} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (K : HomologicalComplex V c) (hK : ∀ (n : ι), P (K.X n)) (i j : ι) : (liftObjectProperty P K hK).d i j = CategoryTheory.ObjectProperty.homMk (K.d i j)

def HomologicalComplex.liftFunctorObjectProperty {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {ι : Type u_2} {c : ComplexShape ι} {V : Type u_3} [CategoryTheory.Category.{v_2, u_3} V] [CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (F : CategoryTheory.Functor D (HomologicalComplex V c)) (hF : ∀ (X : D) (n : ι), P ((F.obj X).X n)) : CategoryTheory.Functor D (HomologicalComplex P.FullSubcategory c)

The functor D ⥤ HomologicalComplex P.FullSubcategory c which is obtained by lifting a functor D ⥤ HomologicalComplex V c when for any X : D and n, the object (F.obj X).X n satisfies a property P : ObjectProperty V.

Equations

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

@[simp]

theorem HomologicalComplex.liftFunctorObjectProperty_obj {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {ι : Type u_2} {c : ComplexShape ι} {V : Type u_3} [CategoryTheory.Category.{v_2, u_3} V] [CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (F : CategoryTheory.Functor D (HomologicalComplex V c)) (hF : ∀ (X : D) (n : ι), P ((F.obj X).X n)) (X : D) : (liftFunctorObjectProperty P F hF).obj X = liftObjectProperty P (F.obj X) ⋯

@[simp]

theorem HomologicalComplex.liftFunctorObjectProperty_map_f {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {ι : Type u_2} {c : ComplexShape ι} {V : Type u_3} [CategoryTheory.Category.{v_2, u_3} V] [CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (F : CategoryTheory.Functor D (HomologicalComplex V c)) (hF : ∀ (X : D) (n : ι), P ((F.obj X).X n)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (n : ι) : ((liftFunctorObjectProperty P F hF).map f).f n = CategoryTheory.ObjectProperty.homMk ((F.map f).f n)