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

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) : HomologicalComplex.extend.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 (HomologicalComplex.extend.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 : Option ι) (j : Option ι) : HomologicalComplex.extend.X K i ⟶ HomologicalComplex.extend.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 : Option ι) (j : Option ι) (hi : i = none) : HomologicalComplex.extend.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 : Option ι) (j : Option ι) (hj : j = none) : HomologicalComplex.extend.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 : Option ι} {j : Option ι} {a : ι} {b : ι} (hi : i = some a) (hj : j = some b) : HomologicalComplex.extend.d K i j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XIso K hi).hom (CategoryTheory.CategoryStruct.comp (K.d a b) (HomologicalComplex.extend.XIso K hj).inv)

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

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