The extension of a homological complex by an embedding of complex shapes

Given an embedding e : Embedding c c' of complex shapes, and K : HomologicalComplex C c, we define K.extend e : HomologicalComplex C c', and this leads to a functor e.extendFunctor C : HomologicalComplex C c ⥤ HomologicalComplex C c'.

This construction first appeared in the Liquid Tensor Experiment.

noncomputable def HomologicalComplex.extend.X {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) : Option ι → C

Auxiliary definition for the X field of HomologicalComplex.extend.

noncomputable def HomologicalComplex.extend.XIso {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) {i : Option ι} {j : ι} (hj : i = some j) : X K i ≅ K.X j

The isomorphism X K i ≅ K.X j when i = some j.

theorem HomologicalComplex.extend.isZero_X {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) {i : Option ι} (hi : i = none) : CategoryTheory.Limits.IsZero (X K i)

noncomputable def HomologicalComplex.extend.XOpIso {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i : Option ι) : X K.op i ≅ Opposite.op (X K i)

The canonical isomorphism X K.op i ≅ Opposite.op (X K i).

noncomputable def HomologicalComplex.extend.d {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : Option ι) : X K i ⟶ X K j

Auxiliary definition for the d field of HomologicalComplex.extend.

theorem HomologicalComplex.extend.d_none_eq_zero {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : Option ι) (hi : i = none) : d K i j = 0

theorem HomologicalComplex.extend.d_none_eq_zero' {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : Option ι) (hj : j = none) : d K i j = 0

theorem HomologicalComplex.extend.d_eq {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) {i j : Option ι} {a b : ι} (hi : i = some a) (hj : j = some b) : d K i j = CategoryTheory.CategoryStruct.comp (XIso K hi).hom (CategoryTheory.CategoryStruct.comp (K.d a b) (XIso K hj).inv)

theorem HomologicalComplex.extend.XOpIso_hom_d_op {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : Option ι) : CategoryTheory.CategoryStruct.comp (XOpIso K i).hom (d K j i).op = CategoryTheory.CategoryStruct.comp (d K.op i j) (XOpIso K j).hom

theorem HomologicalComplex.extend.XOpIso_hom_d_op_assoc {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : Option ι) {Z : Cᵒᵖ} (h : Opposite.op (X K j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (XOpIso K i).hom (CategoryTheory.CategoryStruct.comp (d K j i).op h) = CategoryTheory.CategoryStruct.comp (d K.op i j) (CategoryTheory.CategoryStruct.comp (XOpIso K j).hom h)

noncomputable def HomologicalComplex.extend.mapX {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : Option ι) : X K i ⟶ X L i

Auxiliary definition for HomologicalComplex.extendMap.

theorem HomologicalComplex.extend.mapX_some {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) {i : Option ι} {a : ι} (hi : i = some a) : mapX φ i = CategoryTheory.CategoryStruct.comp (XIso K hi).hom (CategoryTheory.CategoryStruct.comp (φ.f a) (XIso L hi).inv)

theorem HomologicalComplex.extend.mapX_none {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) {i : Option ι} (hi : i = none) : mapX φ i = 0

noncomputable def HomologicalComplex.extend {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') : HomologicalComplex C c'

Given K : HomologicalComplex C c and e : c.Embedding c', this is the extension of K in HomologicalComplex C c': it is zero in the degrees that are not in the image of e.f.

noncomputable def HomologicalComplex.extendXIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') {i' : ι'} {i : ι} (h : e.f i = i') : (K.extend e).X i' ≅ K.X i

The isomorphism (K.extend e).X i' ≅ K.X i when e.f i = i'.

theorem HomologicalComplex.isZero_extend_X' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (hi' : e.r i' = none) : CategoryTheory.Limits.IsZero ((K.extend e).X i')

theorem HomologicalComplex.isZero_extend_X {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.Limits.IsZero ((K.extend e).X i')

instance HomologicalComplex.instIsStrictlySupportedExtend {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') : (K.extend e).IsStrictlySupported e

theorem HomologicalComplex.extend_d_eq {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j') : (K.extend e).d i' j' = CategoryTheory.CategoryStruct.comp (K.extendXIso e hi).hom (CategoryTheory.CategoryStruct.comp (K.d i j) (K.extendXIso e hj).inv)

theorem HomologicalComplex.extend_d_from_eq_zero {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι') (i : ι) (hi : e.f i = i') (hi' : ¬c.Rel i (c.next i)) : (K.extend e).d i' j' = 0

theorem HomologicalComplex.extend_d_to_eq_zero {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι') (j : ι) (hj : e.f j = j') (hj' : ¬c.Rel (c.prev j) j) : (K.extend e).d i' j' = 0

noncomputable def HomologicalComplex.extendMap {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c') : K.extend e ⟶ L.extend e

Given an embedding e : c.Embedding c' of complexes shapes, this is the morphism K.extend e ⟶ L.extend e induced by a morphism K ⟶ L in HomologicalComplex C c.

theorem HomologicalComplex.extendMap_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c') {i : ι} {i' : ι'} (h : e.f i = i') : (extendMap φ e).f i' = CategoryTheory.CategoryStruct.comp (K.extendXIso e h).hom (CategoryTheory.CategoryStruct.comp (φ.f i) (L.extendXIso e h).inv)

theorem HomologicalComplex.extendMap_f_eq_zero {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c') (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : (extendMap φ e).f i' = 0

@[simp]

theorem HomologicalComplex.extendMap_comp {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') : extendMap (CategoryTheory.CategoryStruct.comp φ φ') e = CategoryTheory.CategoryStruct.comp (extendMap φ e) (extendMap φ' e)

theorem HomologicalComplex.extendMap_comp_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') {Z : HomologicalComplex C c'} (h : M.extend e ⟶ Z) : CategoryTheory.CategoryStruct.comp (extendMap (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (extendMap φ e) (CategoryTheory.CategoryStruct.comp (extendMap φ' e) h)

theorem HomologicalComplex.extendMap_id_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') : (extendMap (CategoryTheory.CategoryStruct.id K) e).f i' = CategoryTheory.CategoryStruct.id ((K.extend e).X i')

@[simp]

theorem HomologicalComplex.extendMap_id {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') : extendMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.extend e)

@[simp]

theorem HomologicalComplex.extendMap_zero {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K L : HomologicalComplex C c) (e : c.Embedding c') : extendMap 0 e = 0

noncomputable def HomologicalComplex.extendOpIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') : K.op.extend e.op ≅ (K.extend e).op

The canonical isomorphism K.op.extend e.op ≅ (K.extend e).op.

theorem HomologicalComplex.extend_op_d {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι') : (K.op.extend e.op).d i' j' = CategoryTheory.CategoryStruct.comp ((K.extendOpIso e).hom.f i') (CategoryTheory.CategoryStruct.comp ((K.extend e).d j' i').op ((K.extendOpIso e).inv.f j'))

theorem HomologicalComplex.extend_op_d_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι') {Z : Cᵒᵖ} (h : (K.op.extend e.op).X j' ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.op.extend e.op).d i' j') h = CategoryTheory.CategoryStruct.comp ((K.extendOpIso e).hom.f i') (CategoryTheory.CategoryStruct.comp ((K.extend e).d j' i').op (CategoryTheory.CategoryStruct.comp ((K.extendOpIso e).inv.f j') h))

@[simp]

theorem HomologicalComplex.extendMap_add {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} (φ φ' : K ⟶ L) (e : c.Embedding c') : extendMap (φ + φ') e = extendMap φ e + extendMap φ' e

noncomputable def ComplexShape.Embedding.extendFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (HomologicalComplex C c) (HomologicalComplex C c')

Given an embedding e : c.Embedding c' of complex shapes, this is the functor HomologicalComplex C c ⥤ HomologicalComplex C c' which extend complexes along e: the extended complexes are zero in the degrees that are not in the image of e.f.

@[simp]

theorem ComplexShape.Embedding.extendFunctor_obj {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) : (e.extendFunctor C).obj K = K.extend e

@[simp]

theorem ComplexShape.Embedding.extendFunctor_map {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X✝ Y✝ : HomologicalComplex C c} (φ : X✝ ⟶ Y✝) : (e.extendFunctor C).map φ = HomologicalComplex.extendMap φ e

instance ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexExtendFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : (e.extendFunctor C).PreservesZeroMorphisms

instance ComplexShape.Embedding.instAdditiveHomologicalComplexExtendFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] : (e.extendFunctor C).Additive