Reindexing finite matrix tuples

noncomputable def MagnitudeConjecture.CategoryTheory.matrixTupleReindexIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : Type} [Fintype I] [Fintype J] (e : J ≃ I) (X : I → C) : { ι := J, fintype := inst✝, X := X ∘ ⇑e } ≅ { ι := I, fintype := inst✝¹, X := X }

A change of finite index set gives an isomorphism of matrix tuples.

noncomputable def MagnitudeConjecture.CategoryTheory.matrixTupleReindexEndAlgEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {I J : Type} [Fintype I] [Fintype J] (e : J ≃ I) (X : I → C) : CategoryTheory.End { ι := J, fintype := inst✝, X := X ∘ ⇑e } ≃ₐ[k] CategoryTheory.End { ι := I, fintype := inst✝¹, X := X }

Reindexing a finite tuple preserves its endomorphism algebra.