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.
@[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_1 : ι), (K.restriction e).d x x_1 = K.d (e.f x) (e.f x_1)
@[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.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]
:
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' := ⋯ }
Instances For
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 ⋯
Instances For
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))
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)
@[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 : HomologicalComplex C c'}
{L : HomologicalComplex C c'}
(φ : K ⟶ L)
(e : c.Embedding c')
[e.IsRelIff]
(i : ι)
:
(HomologicalComplex.restrictionMap φ e).f i = φ.f (e.f i)
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 : HomologicalComplex C c'}
{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' := ⋯ }
Instances For
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 : HomologicalComplex C c'}
{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 ((HomologicalComplex.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))
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 : HomologicalComplex C c'}
{L : HomologicalComplex C c'}
(φ : K ⟶ L)
(e : c.Embedding c')
[e.IsRelIff]
{i : ι}
{i' : ι'}
(hi : e.f i = i')
:
(HomologicalComplex.restrictionMap φ e).f i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).hom
(CategoryTheory.CategoryStruct.comp (φ.f i') (L.restrictionXIso e hi).inv)
@[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]
:
HomologicalComplex.restrictionMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.restriction 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)
:
@[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]
:
@[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
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.
Instances For
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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯