Finite Krull--Schmidt matrices

An endomorphism of a finite biproduct of pairwise nonisomorphic indecomposables with local endomorphism rings is invertible as soon as every diagonal component is invertible. This is the finite-support matrix lemma in the Krull--Schmidt--Warfield argument used by Gabriel's Lemma 3.5.

theorem MagnitudeConjecture.CategoryTheory.isIso_of_isSplitMono_to_indecomposable {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X Y : C} (hY : CategoryTheory.Indecomposable Y) (j : X ⟶ Y) [CategoryTheory.IsSplitMono j] (hX : ¬CategoryTheory.Limits.IsZero X) : CategoryTheory.IsIso j

A split subobject of an indecomposable object is the whole object when its source is nonzero.

theorem MagnitudeConjecture.CategoryTheory.isIso_of_isSplitEpi_from_indecomposable {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X Y : C} (hX : CategoryTheory.Indecomposable X) (p : X ⟶ Y) [CategoryTheory.IsSplitEpi p] (hY : ¬CategoryTheory.Limits.IsZero Y) : CategoryTheory.IsIso p

A split quotient of an indecomposable object is the whole object when its target is nonzero.

theorem MagnitudeConjecture.CategoryTheory.isIso_of_isUnit_preadditiveEnd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} (f : X ⟶ X) (hf : IsUnit (CategoryTheory.End.of f)) : CategoryTheory.IsIso f

A unit for the preadditive-ring structure on an endomorphism is a categorical isomorphism. This bridges Mathlib's two monoid instances on categorical endomorphisms.

theorem MagnitudeConjecture.CategoryTheory.isIso_or_isIso_of_add_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} [IsLocalRing (CategoryTheory.End X)] (f g : X ⟶ X) (hfg : f + g = CategoryTheory.CategoryStruct.id X) : CategoryTheory.IsIso f ∨ CategoryTheory.IsIso g

In a local categorical endomorphism ring, one of two endomorphisms whose sum is the identity is an isomorphism.

theorem MagnitudeConjecture.CategoryTheory.isRadicalMorphism_of_indecomposable_of_not_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X Y : C} (hX : CategoryTheory.Indecomposable X) (hY : CategoryTheory.Indecomposable Y) [IsLocalRing (CategoryTheory.End X)] (hXY : ¬Nonempty (X ≅ Y)) (f : X ⟶ Y) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f

Every morphism between nonisomorphic indecomposables is radical when the source has local endomorphism ring.

theorem MagnitudeConjecture.CategoryTheory.isIso_of_finBiproduct_diagonal_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {J : Type w} [Fintype J] (X : J → C) (hX : ∀ (i : J), CategoryTheory.Indecomposable (X i)) (hlocal : ∀ (i : J), IsLocalRing (CategoryTheory.End (X i))) (hpair : ∀ (i j : J), i ≠ j → ¬Nonempty (X i ≅ X j)) (f : ⨁ X ⟶ ⨁ X) (hdiag : ∀ (i : J), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π X i)))) : CategoryTheory.IsIso f

A finite Krull--Schmidt matrix is invertible whenever all its diagonal entries are invertible.