Documentation

Mathlib.Algebra.Homology.FullSubcategory

Homological complexes in full subcategories #

source
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.
Instances For
    source
    @[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 := ⋯ }
    source
    @[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)
    source
    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.
    Instances For
      source
      @[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) ⋯
      source
      @[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)