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.

Equations

• HomologicalComplex.extend.X K (some x_1) = K.X x_1
• HomologicalComplex.extend.X K none = 0

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.

Equations

• HomologicalComplex.extend.XIso K hj = CategoryTheory.eqToIso ⋯

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).

Equations

• HomologicalComplex.extend.XOpIso K (some x_1) = CategoryTheory.Iso.refl (HomologicalComplex.extend.X K.op (some x_1))
• HomologicalComplex.extend.XOpIso K none = ⋯.iso ⋯

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.

Equations

• HomologicalComplex.extend.d K none x✝ = 0
• HomologicalComplex.extend.d K (some i) (some j) = K.d i j
• HomologicalComplex.extend.d K (some val) none = 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 ι) (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.

Equations

• HomologicalComplex.extend.mapX φ (some x_1) = φ.f x_1
• HomologicalComplex.extend.mapX φ none = 0

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.

Equations

• K.extend e = { X := fun (i' : ι') => HomologicalComplex.extend.X K (e.r i'), d := fun (i' j' : ι') => HomologicalComplex.extend.d K (e.r i') (e.r j'), shape := ⋯, d_comp_d' := ⋯ }

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'.

Equations

• K.extendXIso e h = HomologicalComplex.extend.XIso K ⋯

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 ambedding 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.

Equations

• HomologicalComplex.extendMap φ e = { f := fun (x : ι') => HomologicalComplex.extend.mapX φ (e.r x), comm' := ⋯ }

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.

Equations

• K.extendOpIso e = HomologicalComplex.Hom.isoOfComponents (fun (x : ι') => HomologicalComplex.extend.XOpIso K (e.op.r x)) ⋯

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.

Equations

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

@[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