Lemma 2.5: strict radical layers

Lemma 2.5 (lem:strict-radical-layers, graded-category.tex). Let J be the radical of the category of finite-length modules and let a : U → Y be a radical monomorphism such that a + h is monic for every h ∈ J²(U, Y). Then for every W and n ≥ 1, a ∘ z ∈ J^n(W, Y) ⇔ z ∈ J^{n-1}(W, U). Every direct sum of left almost split inclusions satisfies the hypothesis.

This file proves the lemma in an additive category with kernels and binary biproducts, for the categorical radical ideal I (the vendored homIdeal) and its powers, under two hypotheses which hold for mod A:

• every object Y has a right radical approximation: a radical map p : E → Y through which every radical map into Y factors, with a radical monic kernel i : T → E such that every map in I²(T, Z) is i ≫ q with q radical (in the manuscript, p is the sum of the minimal right almost split maps of the summands of Y, with rad P → P at projective summands, and i is a sum of left almost split inclusions);
• the Krull–Schmidt normal form: every map becomes, after an isomorphism of its source, a row of a split monomorphism and a radical map (the manuscript's "split off the invertible blocks of u").

The proof is the manuscript's: the identity p ∘ J^n(W, E) = J^{n+1}(W, Y) (eq:right-radical-surjection), splitting off the given monomorphism, the complementary monomorphism b with the same perturbation property, and induction on the radical degree for all such monomorphisms simultaneously. In Lean composition is written z ≫ a for the manuscript's a ∘ z, and the exponents are shifted: z ≫ a ∈ I^{n+1} implies z ∈ I^n.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.StrictLayers.Ipow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℕ) : MBDVendor.QSE.CategoricalIdeal.HomIdeal C

The n-th power of the categorical radical.

theorem MultiplicativeBasisDeformations.StrictLayers.mem_Ipow_one_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) : f ∈ (Ipow 1).hom X Y ↔ MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f

theorem MultiplicativeBasisDeformations.StrictLayers.rad_comp_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f) {n : ℕ} (hg : g ∈ (Ipow n).hom Y Z) : CategoryTheory.CategoryStruct.comp f g ∈ (Ipow (n + 1)).hom X Z

A radical map followed by a map of I^n lies in I^{n+1}.

theorem MultiplicativeBasisDeformations.StrictLayers.comp_rad_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y Z : C} {n : ℕ} {f : X ⟶ Y} (hf : f ∈ (Ipow n).hom X Y) {g : Y ⟶ Z} (hg : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism g) : CategoryTheory.CategoryStruct.comp f g ∈ (Ipow (n + 1)).hom X Z

A map of I^n followed by a radical map lies in I^{n+1}.

theorem MultiplicativeBasisDeformations.StrictLayers.rad_comp_rad_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f) (hg : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism g) : CategoryTheory.CategoryStruct.comp f g ∈ (Ipow 2).hom X Z

theorem MultiplicativeBasisDeformations.StrictLayers.mem_Ipow_of_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {n : ℕ} {f : X ⟶ Y} (hf : f ∈ (Ipow (n + 1)).hom X Y) : f ∈ (Ipow n).hom X Y

theorem MultiplicativeBasisDeformations.StrictLayers.isIso_one_add_of_rad {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} {q : X ⟶ X} (hq : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism q) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X + q)

1 + q is invertible for a radical endomorphism q.

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

A right radical approximation of Y (see the module docstring).

• 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
• sq {Z : C} (g : self.T ⟶ Z) : g ∈ (Ipow 2).hom self.T Z → ∃ (q : self.E ⟶ Z), MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism q ∧ CategoryTheory.CategoryStruct.comp self.i q = g

def MultiplicativeBasisDeformations.StrictLayers.HasSplitRadicalNormalForm (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : Prop

The Krull–Schmidt split–radical normal form.

theorem MultiplicativeBasisDeformations.StrictLayers.RightRadicalApprox.exists_lift_of_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y : C} (P : RightRadicalApprox Y) {W : C} {n : ℕ} {g : W ⟶ Y} (hg : g ∈ (Ipow (n + 1)).hom W Y) : ∃ w ∈ (Ipow n).hom W P.E, CategoryTheory.CategoryStruct.comp w P.p = g

eq:right-radical-surjection: every map of I^{n+1}(W, Y) is w ≫ p with w ∈ I^n(W, E).

theorem MultiplicativeBasisDeformations.StrictLayers.isSplitMono_of_perturbation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (hnf : HasSplitRadicalNormalForm C) {U E Y : C} (u : U ⟶ E) (p : E ⟶ Y) (hp : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism p) (hpert : ∀ h ∈ (Ipow 2).hom U Y, CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp u p + h)) : CategoryTheory.IsSplitMono u

Splitting off: if u ≫ p = a with a having the perturbation property and p radical, then u is a split monomorphism.

theorem MultiplicativeBasisDeformations.StrictLayers.strict {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] (hnf : HasSplitRadicalNormalForm C) (approx : (Y : C) → RightRadicalApprox Y) (n : ℕ) {U Y : C} (a : U ⟶ Y) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism a → (∀ h ∈ (Ipow 2).hom U Y, CategoryTheory.Mono (a + h)) → ∀ {W : C} (z : W ⟶ U), CategoryTheory.CategoryStruct.comp z a ∈ (Ipow (n + 1)).hom W Y → z ∈ (Ipow n).hom W U

Lemma 2.5 (lem:strict-radical-layers), abstract form. Let a : U ⟶ Y be radical with a + h monic for every h ∈ I²(U, Y). Then z ≫ a ∈ I^{n+1}(W, Y) implies z ∈ I^n(W, U).

theorem MultiplicativeBasisDeformations.StrictLayers.comp_mem_of_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] {U Y W : C} {a : U ⟶ Y} (ha : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism a) {n : ℕ} {z : W ⟶ U} (hz : z ∈ (Ipow n).hom W U) : CategoryTheory.CategoryStruct.comp z a ∈ (Ipow (n + 1)).hom W Y

The reverse implication of Lemma 2.5: z ∈ I^n implies z ≫ a ∈ I^{n+1} for radical a.

theorem MultiplicativeBasisDeformations.StrictLayers.perturbation_of_factor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {T E : C} (i : T ⟶ E) [CategoryTheory.Mono i] (hsq : ∀ g ∈ (Ipow 2).hom T E, ∃ (q : E ⟶ E), MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism q ∧ CategoryTheory.CategoryStruct.comp i q = g) (h : T ⟶ E) : h ∈ (Ipow 2).hom T E → CategoryTheory.Mono (i + h)

A left almost-split-type map i (every map of I² out of its source factors as i ≫ q with q radical) satisfies the perturbation hypothesis of Lemma 2.5: i + h = i ≫ (1 + q) is monic for every h ∈ I².

theorem MultiplicativeBasisDeformations.StrictLayers.RightRadicalApprox.i_perturbation {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] {Y : C} (P : RightRadicalApprox Y) (h : P.T ⟶ P.E) : h ∈ (Ipow 2).hom P.T P.E → CategoryTheory.Mono (P.i + h)

The kernel map of a right radical approximation has the perturbation property of Lemma 2.5.

theorem MultiplicativeBasisDeformations.StrictLayers.RightRadicalApprox.layer_injective {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] {Y : C} (P : RightRadicalApprox Y) (hnf : HasSplitRadicalNormalForm C) (approx : (Y : C) → RightRadicalApprox Y) {W : C} {n : ℕ} (z : W ⟶ P.T) (hz : CategoryTheory.CategoryStruct.comp z P.i ∈ (Ipow (n + 2)).hom W P.E) : z ∈ (Ipow (n + 1)).hom W P.T

Injectivity on layers (Prop 2.6(1), first map): z ≫ i ∈ I^{n+2} implies z ∈ I^{n+1}.

theorem MultiplicativeBasisDeformations.StrictLayers.RightRadicalApprox.layer_exact {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] {Y : C} (P : RightRadicalApprox Y) (hnf : HasSplitRadicalNormalForm C) (approx : (Y : C) → RightRadicalApprox Y) {W : C} {n : ℕ} (w : W ⟶ P.E) (hw : w ∈ (Ipow (n + 1)).hom W P.E) (hwp : CategoryTheory.CategoryStruct.comp w P.p ∈ (Ipow (n + 3)).hom W Y) : ∃ z ∈ (Ipow n).hom W P.T, w - CategoryTheory.CategoryStruct.comp z P.i ∈ (Ipow (n + 2)).hom W P.E

Exactness at the middle term on layers (Prop 2.6(1)): if w ∈ I^{n+1} and w ≫ p ∈ I^{n+3}, then w ≡ z ≫ i modulo I^{n+2} for some z ∈ I^n.

theorem MultiplicativeBasisDeformations.StrictLayers.RightRadicalApprox.layer_exact_zero {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasKernels C] {Y : C} (P : RightRadicalApprox Y) {W : C} (w : W ⟶ P.E) (hwp : CategoryTheory.CategoryStruct.comp w P.p ∈ (Ipow 2).hom W Y) : w ∈ (Ipow 1).hom W P.E

The lowest degree (Prop 2.6(1)): w ≫ p ∈ I² implies w ∈ I.