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.{v_1, 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 ι)
:
Auxiliary definition for Homotopy.extend
Equations
Instances For
theorem
Homotopy.extend.homAux_eq
{ι : Type u_1}
{c : ComplexShape ι}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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.{v_1, 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' : ι')
:
Auxiliary defnition for Homotopy.extend.
Equations
Instances For
theorem
Homotopy.extend.hom_eq_zero₁
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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')
:
theorem
Homotopy.extend.hom_eq_zero₂
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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')
:
theorem
Homotopy.extend.hom_eq
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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.{v_1, 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]
:
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
Instances For
theorem
Homotopy.extend_hom_eq
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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.{v_1, 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
Instances For
theorem
Homotopy.ofExtend_hom
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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.{v_1, 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))
:
@[simp]
theorem
Homotopy.ofExtend_extend
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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]
:
noncomputable def
Homotopy.extendEquiv
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{v_1, 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]
:
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
Instances For
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.{v_1, 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
Instances For
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.{v_1, 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
Instances For
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.{v_1, 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.{v_1, u_3} C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
: