Categorical indecomposability from a local endomorphism ring

In a preadditive category with binary biproducts, a local endomorphism ring forces categorical indecomposability. This is a bounded adaptation of the generic lemma in the donor's RepresentationDirected/IyamaWordMeshAdditiveHull.lean at commit d5ba0c48e7a851afd51247ff9cd81fc629e00ed2; no word-mesh layer is imported.

theorem MagnitudeConjecture.CategoryTheory.indecomposable_iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} (e : X ≅ Y) : CategoryTheory.Indecomposable X ↔ CategoryTheory.Indecomposable Y

Categorical indecomposability is invariant under isomorphism.

theorem MagnitudeConjecture.CategoryTheory.indecomposable_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) : CategoryTheory.Indecomposable (Opposite.op X) ↔ CategoryTheory.Indecomposable X

Passing to the opposite category preserves and reflects categorical indecomposability.

theorem MagnitudeConjecture.CategoryTheory.indecomposable_of_fully_faithful_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [F.Faithful] (X : C) (hX : CategoryTheory.Indecomposable (F.obj X)) : CategoryTheory.Indecomposable X

A fully faithful additive functor reflects indecomposability from the image of an object.

theorem MagnitudeConjecture.CategoryTheory.indecomposable_map_iff_of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [F.IsEquivalence] (X : C) : CategoryTheory.Indecomposable (F.obj X) ↔ CategoryTheory.Indecomposable X

An additive equivalence preserves and reflects indecomposability.

theorem MagnitudeConjecture.CategoryTheory.indecomposable_of_local_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) [IsLocalRing (CategoryTheory.End X)] : CategoryTheory.Indecomposable X

A nontrivial local endomorphism ring rules out a nontrivial binary biproduct decomposition.

theorem MagnitudeConjecture.RingEquiv.isLocalRing_noncomm {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] [IsLocalRing R] (e : R ≃+* S) : IsLocalRing S

Localness transports across a ring equivalence without a commutativity hypothesis.