The restriction functor of an embedding of complex shapes

Given c and c' complex shapes on two types, and e : c.Embedding c' (satisfying [e.IsRelIff]), we define the restriction functor e.restrictionFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c.

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

Given K : HomologicalComplex C c' and e : c.Embedding c' (satisfying [e.IsRelIff]), this is the homological complex in HomologicalComplex C c obtained by restriction.

Equations

• K.restriction e = { X := fun (i : ι) => K.X (e.f i), d := fun (x x_1 : ι) => K.d (e.f x) (e.f x_1), shape := ⋯, d_comp_d' := ⋯ }

@[simp]

theorem HomologicalComplex.restriction_d {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (x✝ x✝¹ : ι) : (K.restriction e).d x✝ x✝¹ = K.d (e.f x✝) (e.f x✝¹)

@[simp]

theorem HomologicalComplex.restriction_X {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] (i : ι) : (K.restriction e).X i = K.X (e.f i)

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

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

Equations

• K.restrictionXIso e h = CategoryTheory.eqToIso ⋯

theorem HomologicalComplex.restriction_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.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] {i j : ι} {i' j' : ι'} (hi : e.f i = i') (hj : e.f j = j') : (K.restriction e).d i j = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom (CategoryTheory.CategoryStruct.comp (K.d i' j') (K.restrictionXIso e hj).inv)

theorem HomologicalComplex.restriction_d_eq_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] {i j : ι} {i' j' : ι'} (hi : e.f i = i') (hj : e.f j = j') {Z : C} (h : (K.restriction e).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.restriction e).d i j) h = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom (CategoryTheory.CategoryStruct.comp (K.d i' j') (CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj).inv h))

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

The morphism K.restriction e ⟶ L.restriction e induced by a morphism φ : K ⟶ L.

Equations

• HomologicalComplex.restrictionMap φ e = { f := fun (i : ι) => φ.f (e.f i), comm' := ⋯ }

@[simp]

theorem HomologicalComplex.restrictionMap_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsRelIff] (i : ι) : (restrictionMap φ e).f i = φ.f (e.f i)

theorem HomologicalComplex.restrictionMap_f' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsRelIff] {i : ι} {i' : ι'} (hi : e.f i = i') : (restrictionMap φ e).f i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom (CategoryTheory.CategoryStruct.comp (φ.f i') (L.restrictionXIso e hi).inv)

theorem HomologicalComplex.restrictionMap_f'_assoc {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [e.IsRelIff] {i : ι} {i' : ι'} (hi : e.f i = i') {Z : C} (h : (L.restriction e).X i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((restrictionMap φ e).f i) h = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom (CategoryTheory.CategoryStruct.comp (φ.f i') (CategoryTheory.CategoryStruct.comp (L.restrictionXIso e hi).inv h))

@[simp]

theorem HomologicalComplex.restrictionMap_id {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsRelIff] : restrictionMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.restriction e)

@[simp]

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

theorem HomologicalComplex.restrictionMap_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.HasZeroMorphisms C] (K : HomologicalComplex C c') {L : HomologicalComplex C c'} (M : HomologicalComplex C c') (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [e.IsRelIff] {Z : HomologicalComplex C c} (h : M.restriction e ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictionMap (CategoryTheory.CategoryStruct.comp φ φ') e) h = CategoryTheory.CategoryStruct.comp (restrictionMap φ e) (CategoryTheory.CategoryStruct.comp (restrictionMap φ' e) h)

noncomputable def ComplexShape.Embedding.restrictionFunctor {ι : 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] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c)

Given e : ComplexShape.Embedding c c', this is the restriction functor HomologicalComplex C c' ⥤ HomologicalComplex C c.

Equations

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

@[simp]

theorem ComplexShape.Embedding.restrictionFunctor_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] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') : (e.restrictionFunctor C).obj K = K.restriction e

@[simp]

theorem ComplexShape.Embedding.restrictionFunctor_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] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] {X✝ Y✝ : HomologicalComplex C c'} (φ : X✝ ⟶ Y✝) : (e.restrictionFunctor C).map φ = HomologicalComplex.restrictionMap φ e

instance ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor {ι : 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] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] : (e.restrictionFunctor C).PreservesZeroMorphisms

instance ComplexShape.Embedding.instAdditiveHomologicalComplexRestrictionFunctor {ι : 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] [e.IsRelIff] [CategoryTheory.Preadditive C] : (e.restrictionFunctor C).Additive