English
Let C be a preadditive category with finite biproducts, and suppose each End(s_i) has invariant basis number. If two finite direct sums ⨁ s(f(a)) and ⨁ s(g(b)) are isomorphic, then the multiplicities along the index sets are the same up to a bijection; more precisely there exists an equivalence e: α ≃ β such that g (e(a)) = f(a) for all a.
Русский
Пусть C — прэдобавитивная категория с конечными би-продуктами и пусть каждый End(s_i) имеет свойство инвариантной базы. Если два конечных прямых суммирования ⨁ s(f(a)) и ⨁ s(g(b)) из семейства s и индексов α, β изоморфны, тогда мультипликаторные коэффициенты совпадают по существу: существует биекция e: α ≃ β такая, что для каждого a верно g(e(a)) = f(a).
LaTeX
$$$$\exists e:\alpha \cong \beta,\ \forall a:\alpha,\ g(e(a)) = f(a).$$$$
Lean4
/-- Given a hom orthogonal family `s : ι → C`
for which each `End (s i)` is a ring with invariant basis number (e.g. if each `s i` is simple),
if two direct sums over `s` are isomorphic, then they have the same multiplicities.
-/
theorem equiv_of_iso (o : HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι} {g : β → ι}
(i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)) : ∃ e : α ≃ β, ∀ a, g (e a) = f a := by
classical
refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
intro c
apply Nonempty.some
apply Cardinal.eq.1
cases nonempty_fintype α; cases nonempty_fintype β
simp only [Cardinal.mk_fintype, Nat.cast_inj]
exact
Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
(by
rw [← o.matrixDecomposition_comp]
simp)
(by
rw [← o.matrixDecomposition_comp]
simp)
