Truncating a complex by one

Stream: Is there code for X?

[Andrew Yang]

Suppose I have a CochainComplex C ℕ : $A^0 \to A^1 \to A^2 \to \cdots$. How can I get the complex $A^1 \to A^2 \to \cdots$? Should I define a ComplexShape.Embedding to do so? Or is there an existing machinery to deal with this?

[Edward van de Meent]

you mean docs#ComplexShape.Embedding ?

[Edward van de Meent]

(ah, you were talking about defining a specific value of the type, not the type itself)

[Edward van de Meent]

looking at the docs, i suspect that you'd go through docs#HomologicalComplex.restriction ?

[Edward van de Meent]

this seems like a good place to start? i'm not sure it uses correct mathlibisms, but at least the type is correct :upside_down:

import Mathlib
open CategoryTheory Limits

variable {C : Type*} [Category C] [HasZeroMorphisms C] (CP : CochainComplex C ℕ)

@[simps]
def ComplexShape.embeddingPNatNat : ComplexShape.Embedding (up PNat) (up Nat) where
  f := PNat.val
  injective_f := PNat.coe_injective
  rel := by simp

instance : (ComplexShape.embeddingPNatNat).IsTruncGE where
  rel' := by
    simp only [ComplexShape.embeddingPNatNat_f, ComplexShape.up_Rel]
    exact fun i₁ i₂ h => Eq.symm (PNat.eq (id (Eq.symm h)))
  mem_next := by
    simp only [ComplexShape.embeddingPNatNat_f, ComplexShape.up_Rel, forall_eq']
    intro j
    use j + 1
    simp

example : CochainComplex C PNat := CP.restriction (ComplexShape.embeddingPNatNat)