feat(Algebra/Homology): embeddings of complex shapes

[joelriou]

Given two complex shapes c : ComplexShape ι and c' : ComplexShape ι' for homological complexes, an embedding from c to c' (e : c.Embedding c') consists of the data of an injective map f : ι → ι' such that for all i₁ i₂ : ι, c.Rel i₁ i₂ implies c'.Rel (e.f i₁) (e.f i₂).

This notion was originally introduced in the Liquid Tensor Experiment. It shall be further expanded in order to formalize truncation functors on the derived category.

---