Documentation

Mathlib.Algebra.Homology.Embedding.TruncGE

The canonical truncation #

Given an embedding e : Embedding c c' of complex shapes which satisfies e.IsTruncGE and K : HomologicalComplex C c', we define K.truncGE' e : HomologicalComplex C c and K.truncGE e : HomologicalComplex C c' which are the canonical truncations of K relative to e.

For example, if e is the embedding embeddingUpIntGE p of ComplexShape.up in ComplexShape.up which sends n : ℕ to p + n and K : CochainComplex C ℤ, then K.truncGE' e : CochainComplex C ℕ is the following complex:

Q ⟶ K.X (p + 1) ⟶ K.X (p + 2) ⟶ K.X (p + 3) ⟶ ...

where in degree 0, the object Q identifies to the cokernel of K.X (p - 1) ⟶ K.X p (this is K.opcycles p). Then, the cochain complex K.truncGE e is indexed by , and has the following shape:

... ⟶ 0 ⟶ 0 ⟶ 0 ⟶ Q ⟶ K.X (p + 1) ⟶ K.X (p + 2) ⟶ K.X (p + 3) ⟶ ...

where Q is in degree p.

TODO #

noncomputable def HomologicalComplex.truncGE'.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') [∀ (i' : ι'), K.HasHomology i'] (i : ι) :
C

The X field of truncGE'.

Equations
Instances For
    noncomputable def HomologicalComplex.truncGE'.XIsoOpcycles {ι : 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') [∀ (i' : ι'), K.HasHomology i'] {i : ι} (hi : e.BoundaryGE i) :
    HomologicalComplex.truncGE'.X K e i K.opcycles (e.f i)

    The isomorphism truncGE'.X K e i ≅ K.opcycles (e.f i) when e.BoundaryGE i holds.

    Equations
    Instances For
      noncomputable def HomologicalComplex.truncGE'.XIso {ι : 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') [∀ (i' : ι'), K.HasHomology i'] {i : ι} (hi : ¬e.BoundaryGE i) :

      The isomorphism truncGE'.X K e i ≅ K.X (e.f i) when e.BoundaryGE i does not hold.

      Equations
      Instances For
        noncomputable def HomologicalComplex.truncGE'.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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] (i : ι) (j : ι) :

        The d field of truncGE'.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem HomologicalComplex.truncGE'.d_comp_d_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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] (i : ι) (j : ι) (k : ι) {Z : C} (h : HomologicalComplex.truncGE'.X K e k Z) :
          @[simp]
          theorem HomologicalComplex.truncGE'.d_comp_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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] (i : ι) (j : ι) (k : ι) :
          noncomputable def HomologicalComplex.truncGE' {ι : 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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] :

          The canonical truncation of a homological complex relative to an embedding of complex shapes e which satisfies e.IsTruncGE.

          Equations
          Instances For
            noncomputable def HomologicalComplex.truncGE'XIso {ι : 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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i) :
            (K.truncGE' e).X i K.X i'

            The isomorphism (K.truncGE' e).X i ≅ K.X i' when e.f i = i' and e.BoundaryGE i does not hold.

            Equations
            Instances For
              noncomputable def HomologicalComplex.truncGE'XIsoOpcycles {ι : 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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i) :
              (K.truncGE' e).X i K.opcycles i'

              The isomorphism (K.truncGE' e).X i ≅ K.opcycles i' when e.f i = i' and e.BoundaryGE i holds.

              Equations
              Instances For
                theorem HomologicalComplex.truncGE'_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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {j : ι} (hij : c.Rel i j) {i' : ι'} {j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hi : ¬e.BoundaryGE i) :
                (K.truncGE' e).d i j = CategoryTheory.CategoryStruct.comp (K.truncGE'XIso e hi' hi).hom (CategoryTheory.CategoryStruct.comp (K.d i' j') (K.truncGE'XIso e hj' ).inv)
                theorem HomologicalComplex.truncGE'_d_eq_fromOpcycles {ι : 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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] {i : ι} {j : ι} (hij : c.Rel i j) {i' : ι'} {j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hi : e.BoundaryGE i) :
                (K.truncGE' e).d i j = CategoryTheory.CategoryStruct.comp (K.truncGE'XIsoOpcycles e hi' hi).hom (CategoryTheory.CategoryStruct.comp (K.fromOpcycles i' j') (K.truncGE'XIso e hj' ).inv)
                noncomputable def HomologicalComplex.truncGE {ι : 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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] :

                The canonical truncation of a homological complex relative to an embedding of complex shapes e which satisfies e.IsTruncGE.

                Equations
                • K.truncGE e = (K.truncGE' e).extend e
                Instances For
                  noncomputable def HomologicalComplex.truncGEXIso {ι : 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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i) :
                  (K.truncGE e).X i' K.X i'

                  The isomorphism (K.truncGE e).X i' ≅ K.X i' when e.f i = i' and e.BoundaryGE i does not hold.

                  Equations
                  • K.truncGEXIso e hi' hi = (K.truncGE' e).extendXIso e hi' ≪≫ K.truncGE'XIso e hi' hi
                  Instances For
                    noncomputable def HomologicalComplex.truncGEXIsoOpcycles {ι : 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.IsTruncGE] [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i) :
                    (K.truncGE e).X i' K.opcycles i'

                    The isomorphism (K.truncGE e).X i' ≅ K.opcycles i' when e.f i = i' and e.BoundaryGE i holds.

                    Equations
                    • K.truncGEXIsoOpcycles e hi' hi = (K.truncGE' e).extendXIso e hi' ≪≫ K.truncGE'XIsoOpcycles e hi' hi
                    Instances For