The extension functor on the homotopy categories

Given an embedding of complex shapes e : c.Embedding c' and a preadditive category C, we define a fully faithful functor e.extendHomotopyFunctor C : HomotopyCategory C c ⥤ HomotopyCategory C c'.

noncomputable def Homotopy.extend.homAux {ι : Type u_1} {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} (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : Option ι) : HomologicalComplex.extend.X K i' ⟶ HomologicalComplex.extend.X L j'

Auxiliary definition for Homotopy.extend

Equations

• Homotopy.extend.homAux φ none j' = 0
• Homotopy.extend.homAux φ i' none = 0
• Homotopy.extend.homAux φ (some i) (some j) = φ i j

theorem Homotopy.extend.homAux_eq {ι : Type u_1} {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} (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : Option ι) (i j : ι) (hi : i' = some i) (hj : j' = some j) : homAux φ i' j' = CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XIso K hi).hom (CategoryTheory.CategoryStruct.comp (φ i j) (HomologicalComplex.extend.XIso L hj).inv)

noncomputable def Homotopy.extend.hom {ι : 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} (e : c.Embedding c') (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : ι') : (K.extend e).X i' ⟶ (L.extend e).X j'

Auxiliary defnition for Homotopy.extend.

Equations

• Homotopy.extend.hom e φ i' j' = Homotopy.extend.homAux φ (e.r i') (e.r j')

theorem Homotopy.extend.hom_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.Preadditive C] {K L : HomologicalComplex C c} (e : c.Embedding c') (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : hom e φ i' j' = 0

theorem Homotopy.extend.hom_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.Preadditive C] {K L : HomologicalComplex C c} (e : c.Embedding c') (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : ι') (hj' : ∀ (j : ι), e.f j ≠ j') : hom e φ i' j' = 0

theorem Homotopy.extend.hom_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.Preadditive C] {K L : HomologicalComplex C c} (e : c.Embedding c') (φ : (i j : ι) → K.X i ⟶ L.X j) {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j') : hom e φ i' j' = CategoryTheory.CategoryStruct.comp (K.extendXIso e hi).hom (CategoryTheory.CategoryStruct.comp (φ i j) (L.extendXIso e hj).inv)

noncomputable def Homotopy.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.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) (e : c.Embedding c') [e.IsRelIff] : Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)

If e : c.Embedding c' is an embedding of complex shapes and h is a homotopy between morphisms of homological complexes of shape c, this is the corresponding homotopy between the extension of these morphisms.

Equations

• h.extend e = { hom := Homotopy.extend.hom e h.hom, zero := ⋯, comm := ⋯ }

theorem Homotopy.extend_hom_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.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) (e : c.Embedding c') [e.IsRelIff] {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j') : (h.extend e).hom i' j' = CategoryTheory.CategoryStruct.comp (K.extendXIso e hi).hom (CategoryTheory.CategoryStruct.comp (h.hom i j) (L.extendXIso e hj).inv)

noncomputable def Homotopy.ofExtend {ι : 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} {f g : K ⟶ L} {e : c.Embedding c'} [e.IsRelIff] (h : Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)) : Homotopy f g

If e : c.Embedding c' is an embedding of complex shapes, f and g are morphism between cochain complexes of shape c, and h is an homotopy between the extensions extendMap f e and extendMap g e, then this is the corresponding homotopy between f and g.

Equations

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

theorem Homotopy.ofExtend_hom {ι : 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} {f g : K ⟶ L} {e : c.Embedding c'} [e.IsRelIff] (h : Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)) (i j : ι) : h.ofExtend.hom i j = CategoryTheory.CategoryStruct.comp (K.extendXIso e ⋯).inv (CategoryTheory.CategoryStruct.comp (h.hom (e.f i) (e.f j)) (L.extendXIso e ⋯).hom)

@[simp]

theorem Homotopy.extend_ofExtend {ι : 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} {f g : K ⟶ L} {e : c.Embedding c'} [e.IsRelIff] (h : Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)) : h.ofExtend.extend e = h

@[simp]

theorem Homotopy.ofExtend_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.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) (e : c.Embedding c') [e.IsRelIff] : (h.extend e).ofExtend = h

noncomputable def Homotopy.extendEquiv {ι : 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} {f g : K ⟶ L} (e : c.Embedding c') [e.IsRelIff] : Homotopy f g ≃ Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)

If e : c.Embedding c' is an embedding of complex shapes, f and g are morphism between cochain complexes of shape c, this is the bijection between homotopies between f and g, and homotopies between the extensions extendMap f e and extendMap g e.

Equations

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

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

Given an embedding e : c.Embedding c' of complex shapes, this is the functor HomotopyCategory C c ⥤ HomotopyCategory C c' which extend complexes along e.

Equations

• e.extendHomotopyFunctor C = CategoryTheory.Quotient.lift (homotopic C c) ((e.extendFunctor C).comp (HomotopyCategory.quotient C c')) ⋯

noncomputable def ComplexShape.Embedding.extendHomotopyFunctorFactors {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] : (HomotopyCategory.quotient C c).comp (e.extendHomotopyFunctor C) ≅ (e.extendFunctor C).comp (HomotopyCategory.quotient C c')

Given an embedding e : c.Embedding c' of complex shapes, the functor e.extendHomotopyFunctor C on homotopy categories is induced by the functor e.extendFunctor C on homological complexes.

Equations

• e.extendHomotopyFunctorFactors C = CategoryTheory.Iso.refl ((HomotopyCategory.quotient C c).comp (e.extendHomotopyFunctor C))

instance ComplexShape.Embedding.instFullHomotopyCategoryExtendHomotopyFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] : (e.extendHomotopyFunctor C).Full

instance ComplexShape.Embedding.instFaithfulHomotopyCategoryExtendHomotopyFunctor {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] : (e.extendHomotopyFunctor C).Faithful