Documentation

Mathlib.Algebra.Homology.Embedding.Extend

The extension of a homological complex by an embedding of complex shapes #

Given an embedding e : Embedding c c' of complex shapes, and K : HomologicalComplex C c, we define K.extend e : HomologicalComplex C c'.

This construction first appeared in the Liquid Tensor Experiment.

The isomorphism X K i ≅ K.X j when i = some j.

Equations
Instances For

    Given K : HomologicalComplex C c and e : c.Embedding c', this is the extension of K in HomologicalComplex C c': it is zero in the degrees that are not in the image of e.f.

    Equations
    Instances For
      noncomputable def HomologicalComplex.extendXIso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') {i' : ι'} {i : ι} (h : e.f i = i') :
      (K.extend e).X i' K.X i

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

      Equations
      Instances For
        theorem HomologicalComplex.isZero_extend_X' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (hi' : e.r i' = none) :
        CategoryTheory.Limits.IsZero ((K.extend e).X i')
        theorem HomologicalComplex.isZero_extend_X {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (hi' : ∀ (i : ι), e.f i i') :
        CategoryTheory.Limits.IsZero ((K.extend e).X i')
        theorem HomologicalComplex.extend_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.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') {i' : ι'} {j' : ι'} {i : ι} {j : ι} (hi : e.f i = i') (hj : e.f j = j') :
        (K.extend e).d i' j' = CategoryTheory.CategoryStruct.comp (K.extendXIso e hi).hom (CategoryTheory.CategoryStruct.comp (K.d i j) (K.extendXIso e hj).inv)
        theorem HomologicalComplex.extend_d_from_eq_zero {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (j' : ι') (i : ι) (hi : e.f i = i') (hi' : ¬c.Rel i (c.next i)) :
        (K.extend e).d i' j' = 0
        theorem HomologicalComplex.extend_d_to_eq_zero {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (j' : ι') (j : ι) (hj : e.f j = j') (hj' : ¬c.Rel (c.prev j) j) :
        (K.extend e).d i' j' = 0