Mapping restricted homological complexes

This file provides the comparison between first restricting a homological complex along an embedding of complex shapes and then mapping it, and first mapping the complex and then restricting it. This transports mapped or forgotten complexes through shape reindexing, allowing results about a restricted complex to be compared with the corresponding restriction of the mapped complex.

Main result

• ComplexShape.Embedding.mapRestrictionIso: mapping homological complexes commutes with restriction along a shape embedding.

noncomputable def ComplexShape.Embedding.mapRestrictionIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {ι : Type u_3} {ι' : Type u_4} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [e.IsRelIff] (K : HomologicalComplex C c') : (F.mapHomologicalComplex c).obj ((e.restrictionFunctor C).obj K) ≅ (e.restrictionFunctor D).obj ((F.mapHomologicalComplex c').obj K)

Mapping homological complexes commutes with restriction along a shape embedding. The two composites have definitionally equal objects, so each component is an identity morphism.

Equations

• e.mapRestrictionIso F K = HomologicalComplex.Hom.isoOfComponents (fun (x : ι) => CategoryTheory.Iso.refl (((F.mapHomologicalComplex c).obj ((e.restrictionFunctor C).obj K)).X x)) ⋯

@[simp]

theorem ComplexShape.Embedding.mapRestrictionIso_hom_f {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {ι : Type u_3} {ι' : Type u_4} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [e.IsRelIff] (K : HomologicalComplex C c') (i : ι) : (e.mapRestrictionIso F K).hom.f i = CategoryTheory.CategoryStruct.id (F.obj (K.X (e.f i)))

The forward component of mapRestrictionIso is the identity.

@[simp]

theorem ComplexShape.Embedding.mapRestrictionIso_inv_f {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {ι : Type u_3} {ι' : Type u_4} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [e.IsRelIff] (K : HomologicalComplex C c') (i : ι) : (e.mapRestrictionIso F K).inv.f i = CategoryTheory.CategoryStruct.id (F.obj (K.X (e.f i)))

The inverse component of mapRestrictionIso is the identity.