The Krull–Schmidt split–radical normal form

Proof of Lemma 2.5, "Split off the invertible blocks of u by Krull–Schmidt decomposition and elementary row and column operations" (graded-category.tex), in any preadditive category with finite biproducts whose objects are finite biproducts of nonzero objects with local endomorphism rings (hasSplitRadicalNormalForm_of_decomp). The argument is the vendored one for finite τ-categories (MBDVendor.QSE.Iyama.splitRadicalForm_finBiproduct), with the finite skeleton replaced by this decomposition hypothesis.

structure MultiplicativeBasisDeformations.StrictLayers.SRF {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X M : C} (k : X ⟶ M) : Type (max u v)

A split–radical form of a map k : X → M.

• Z : C
• U : C
• e : X ≅ self.Z ⊞ self.U
• j : self.Z ⟶ M
• r : self.U ⟶ M
• s : M ⟶ self.Z
• j_s : CategoryTheory.CategoryStruct.comp self.j self.s = CategoryTheory.CategoryStruct.id self.Z
• r_s : CategoryTheory.CategoryStruct.comp self.r self.s = 0
• r_rad : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism self.r
• map_eq : CategoryTheory.CategoryStruct.comp self.e.inv k = CategoryTheory.Limits.biprod.desc self.j self.r

noncomputable def MultiplicativeBasisDeformations.StrictLayers.SRF.precomposeIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y M : C} {q : Y ⟶ M} (h : SRF q) (e₀ : X ≅ Y) (k : X ⟶ M) (hk : CategoryTheory.CategoryStruct.comp e₀.inv k = q) : SRF k

Transport along an isomorphism of sources.

theorem MultiplicativeBasisDeformations.StrictLayers.rad_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {U V M : C} {a : U ⟶ M} {r : V ⟶ M} (ha : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism a) (hr : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism r) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (CategoryTheory.Limits.biprod.desc a r)

noncomputable def MultiplicativeBasisDeformations.StrictLayers.srf_biprod_local {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : C) [IsLocalRing (CategoryTheory.End P)] (hP : ¬CategoryTheory.Limits.IsZero P) {Q M : C} (f : P ⟶ M) (q : Q ⟶ M) (hq : SRF q) : SRF (CategoryTheory.Limits.biprod.desc f q)

Adding one local summand to a split–radical form.

noncomputable def MultiplicativeBasisDeformations.StrictLayers.srf_fin {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) (F : Fin n → C) : (∀ (i : Fin n), ¬CategoryTheory.Limits.IsZero (F i) ∧ IsLocalRing (CategoryTheory.End (F i))) → (M : C) → (k : ⨁ F ⟶ M) → SRF k

Split–radical form on a finite biproduct of local objects.

theorem MultiplicativeBasisDeformations.StrictLayers.hasSplitRadicalNormalForm_of_decomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] (hdec : ∀ (X : C), ∃ (n : ℕ) (F : Fin n → C), (∀ (i : Fin n), ¬CategoryTheory.Limits.IsZero (F i) ∧ IsLocalRing (CategoryTheory.End (F i))) ∧ Nonempty (X ≅ ⨁ F)) : HasSplitRadicalNormalForm C

The Krull–Schmidt split–radical normal form in a category whose objects are finite biproducts of nonzero objects with local endomorphism rings.

Right radical approximations from almost split maps

theorem MultiplicativeBasisDeformations.StrictLayers.rad_finsum {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} {ι : Type u_1} (s : Finset ι) (f : ι → (X ⟶ Y)) (h : ∀ i ∈ s, MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (f i)) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (∑ i ∈ s, f i)

theorem MultiplicativeBasisDeformations.StrictLayers.rad_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {A B : Fin n → C} (f : (j : Fin n) → A j ⟶ B j) (h : ∀ (j : Fin n), MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (f j)) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (CategoryTheory.Limits.biproduct.map f)

theorem MultiplicativeBasisDeformations.StrictLayers.rad_descB {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {A : Fin n → C} {Z : C} (f : (j : Fin n) → A j ⟶ Z) (h : ∀ (j : Fin n), MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (f j)) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (CategoryTheory.Limits.biproduct.desc f)

theorem MultiplicativeBasisDeformations.StrictLayers.sq_of_factor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {T E : C} (i : T ⟶ E) (hfac : ∀ {M : C} (u : T ⟶ M), MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism u → ∃ (b : E ⟶ M), CategoryTheory.CategoryStruct.comp i b = u) {Z : C} (g : T ⟶ Z) (hg : g ∈ (Ipow 2).hom T Z) : ∃ (q : E ⟶ Z), MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism q ∧ CategoryTheory.CategoryStruct.comp i q = g

sq from the factorization of radical maps out of T through i.

structure MultiplicativeBasisDeformations.StrictLayers.ARData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) : Type (max u v)

Auslander–Reiten data at an indecomposable (ordinary Auslander–Reiten theory, assumed by the manuscript, main.tex): a right almost split map p : E → Y with kernel i : T → E, where T = 0 (projective Y, p : rad P → P) or i is left almost split from an indecomposable T (the almost split sequence).

• E : C
• T : C
• p : self.E ⟶ Y
• i : self.T ⟶ self.E
• ras : IsRightAlmostSplit self.p
• i_p : CategoryTheory.CategoryStruct.comp self.i self.p = 0
• lift {W : C} (w : W ⟶ self.E) : CategoryTheory.CategoryStruct.comp w self.p = 0 → ∃ (s : W ⟶ self.T), CategoryTheory.CategoryStruct.comp s self.i = w
• mono : CategoryTheory.Mono self.i
• left : CategoryTheory.Limits.IsZero self.T ∨ ¬CategoryTheory.Limits.IsZero self.T ∧ IsLocalRing (CategoryTheory.End self.T) ∧ IsLeftAlmostSplit self.i

structure MultiplicativeBasisDeformations.StrictLayers.Approx {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) : Type (max u v)

A right radical approximation in which every radical map out of T factors through i.

• E : C
• p : self.E ⟶ Y
• T : C
• i : self.T ⟶ self.E
• p_rad : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism self.p
• factors {W : C} (g : W ⟶ Y) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism g → ∃ (g' : W ⟶ self.E), CategoryTheory.CategoryStruct.comp g' self.p = g
• i_p : CategoryTheory.CategoryStruct.comp self.i self.p = 0
• lift {W : C} (w : W ⟶ self.E) : CategoryTheory.CategoryStruct.comp w self.p = 0 → ∃ (s : W ⟶ self.T), CategoryTheory.CategoryStruct.comp s self.i = w
• i_mono : CategoryTheory.Mono self.i
• i_rad : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism self.i
• fac {M : C} (u : self.T ⟶ M) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism u → ∃ (b : self.E ⟶ M), CategoryTheory.CategoryStruct.comp self.i b = u

def MultiplicativeBasisDeformations.StrictLayers.Approx.toRRA {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y : C} (P : Approx Y) : RightRadicalApprox Y

The right radical approximation.

def MultiplicativeBasisDeformations.StrictLayers.approxLocal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {Y : C} [IsLocalRing (CategoryTheory.End Y)] (hY : ¬CategoryTheory.Limits.IsZero Y) (D : ARData Y) : Approx Y

The approximation of an indecomposable, from its Auslander–Reiten data.

noncomputable def MultiplicativeBasisDeformations.StrictLayers.approxBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (F : Fin n → C) (P : (j : Fin n) → Approx (F j)) : Approx (⨁ F)

Approximations of a finite biproduct: the sum of the approximations of the summands.

def MultiplicativeBasisDeformations.StrictLayers.Approx.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {Y Y' : C} (P : Approx Y) (e : Y ≅ Y') : Approx Y'

Approximations transport along isomorphisms.

theorem MultiplicativeBasisDeformations.StrictLayers.perturbation_biproduct_leftAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {T E : Fin n → C} (i : (j : Fin n) → T j ⟶ E j) [hmono : ∀ (j : Fin n), CategoryTheory.Mono (i j)] (hT : ∀ (j : Fin n), ¬CategoryTheory.Limits.IsZero (T j) ∧ IsLocalRing (CategoryTheory.End (T j))) (hi : ∀ (j : Fin n), IsLeftAlmostSplit (i j)) (h : ⨁ T ⟶ ⨁ E) : h ∈ (Ipow 2).hom (⨁ T) (⨁ E) → CategoryTheory.Mono (CategoryTheory.Limits.biproduct.map i + h)

Lemma 2.5, last sentence: every finite direct sum of left almost split inclusions out of indecomposables (nonzero, local endomorphism ring) satisfies the perturbation hypothesis: a + h is monic for every h ∈ J².

Lemma 2.5 in a Krull–Schmidt category with Auslander–Reiten theory

theorem MultiplicativeBasisDeformations.StrictLayers.nonempty_approx {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] (hdec : ∀ (X : C), ∃ (n : ℕ) (F : Fin n → C), (∀ (i : Fin n), ¬CategoryTheory.Limits.IsZero (F i) ∧ IsLocalRing (CategoryTheory.End (F i))) ∧ Nonempty (X ≅ ⨁ F)) (hAR : ∀ (Y : C), ¬CategoryTheory.Limits.IsZero Y → IsLocalRing (CategoryTheory.End Y) → Nonempty (ARData Y)) (X : C) : Nonempty (RightRadicalApprox X)

Every object has a right radical approximation.

theorem MultiplicativeBasisDeformations.StrictLayers.strict_of_AR {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] (hdec : ∀ (X : C), ∃ (n : ℕ) (F : Fin n → C), (∀ (i : Fin n), ¬CategoryTheory.Limits.IsZero (F i) ∧ IsLocalRing (CategoryTheory.End (F i))) ∧ Nonempty (X ≅ ⨁ F)) (hAR : ∀ (Y : C), ¬CategoryTheory.Limits.IsZero Y → IsLocalRing (CategoryTheory.End Y) → Nonempty (ARData Y)) (n : ℕ) {U Y : C} (a : U ⟶ Y) (ha : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism a) (hpert : ∀ h ∈ (Ipow 2).hom U Y, CategoryTheory.Mono (a + h)) {W : C} (z : W ⟶ U) (hz : CategoryTheory.CategoryStruct.comp z a ∈ (Ipow (n + 1)).hom W Y) : z ∈ (Ipow n).hom W U

Lemma 2.5 (lem:strict-radical-layers) in a Krull–Schmidt category (objects are finite biproducts of indecomposables with local endomorphism rings) with Auslander–Reiten theory (right almost split maps at indecomposables, with kernel zero or left almost split): for a radical a : U → Y with a + h monic for all h ∈ J²(U, Y), z ≫ a ∈ J^{n+1} implies z ∈ J^n.