Documentation

Mathlib.Algebra.Homology.Embedding.Restriction

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
    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
      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) :
        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 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
        @[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

        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
          • =