Isomorphism invariance of Euler characteristics

Mathlib's HomologicalComplex.eulerChar and HomologicalComplex.homologyEulerChar are defined as finsums of finranks. This file records that both are invariant under isomorphisms of complexes of modules.

Main results

• HomologicalComplex.eulerChar_eq_of_iso and HomologicalComplex.homologyEulerChar_eq_of_iso: both Euler characteristics are invariant under isomorphisms of complexes.

theorem HomologicalComplex.eulerChar_eq_of_iso {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} [c.EulerCharSigns] {K L : HomologicalComplex (ModuleCat R) c} (e : K ≅ L) : K.eulerChar = L.eulerChar

Isomorphic complexes of modules have the same Euler characteristic.

theorem HomologicalComplex.homologyEulerChar_eq_of_iso {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} [c.EulerCharSigns] {K L : HomologicalComplex (ModuleCat R) c} [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] (e : K ≅ L) : K.homologyEulerChar = L.homologyEulerChar

Isomorphic complexes of modules have the same homology Euler characteristic.