Transporting strict descent of a family through an additive equivalence

theorem MagnitudeConjecture.CategoryTheory.ranked_family_of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (E : C ≌ D) [E.functor.Additive] {ι : Type w} (F : ι → D) (rank : ι → ℤ) (hF : ∀ (i j : ι) (f : F i ⟶ F j), f ≠ 0 → ¬CategoryTheory.IsIso f → rank j < rank i) (i j : ι) (f : E.inverse.obj (F i) ⟶ E.inverse.obj (F j)) (hf : f ≠ 0) (hi : ¬CategoryTheory.IsIso f) : rank j < rank i

Strict descent of nonzero nonisomorphisms is invariant under an additive equivalence.