Finite biproducts of Iyama tau-approximation complexes

This file constructs the explicit componentwise finite biproduct of short complexes. Weak kernels, weak cokernels, and Iyama's radical approximation conditions are preserved. When the categorical radical is represented by a two-sided additive Hom ideal, minimality is also preserved, so both right and left tau-sequences are closed under finite biproducts. The current interface supplies that ideal through NilpotentRadicalData; its nilpotence field is not used by the results in this file.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.shortComplexBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex C

The componentwise finite biproduct of short complexes.

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.shortComplexBiproduct_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) : (shortComplexBiproduct S).f = CategoryTheory.Limits.biproduct.map fun (j : J) => (S j).f

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.shortComplexBiproduct_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) : (shortComplexBiproduct S).g = CategoryTheory.Limits.biproduct.map fun (j : J) => (S j).g

theorem QuotientSubmoduleEquidistribution.Iyama.isWeakKernel_shortComplexBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) (hS : ∀ (j : J), ShortComplex.IsWeakKernel (S j)) : ShortComplex.IsWeakKernel (shortComplexBiproduct S)

Finite componentwise biproducts preserve weak kernels.

theorem QuotientSubmoduleEquidistribution.Iyama.isWeakCokernel_shortComplexBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) (hS : ∀ (j : J), ShortComplex.IsWeakCokernel (S j)) : ShortComplex.IsWeakCokernel (shortComplexBiproduct S)

Finite componentwise biproducts preserve weak cokernels.

theorem QuotientSubmoduleEquidistribution.Iyama.isRadicalMorphism_biproduct_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J : Type w} [Fintype J] {X Y : J → C} (f : (j : J) → X j ⟶ Y j) (hf : ∀ (j : J), CategoricalRadical.IsRadicalMorphism (f j)) : CategoricalRadical.IsRadicalMorphism (CategoryTheory.Limits.biproduct.map f)

A componentwise finite biproduct of radical morphisms is radical once the categorical radical is available as a two-sided additive Hom ideal.

theorem QuotientSubmoduleEquidistribution.Iyama.tauApproximation_shortComplexBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) (hS : ∀ (j : J), TauApproximation (S j)) : TauApproximation (shortComplexBiproduct S)

Tau-approximation conditions are preserved by finite componentwise biproducts. Minimality is deliberately not part of this statement.

theorem QuotientSubmoduleEquidistribution.Iyama.isRadicalMorphism_of_comp_eq_zero_of_isRightMinimal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {W X Y : C} {a : W ⟶ X} {f : X ⟶ Y} (hf : IsRightMinimal f) (ha : CategoryTheory.CategoryStruct.comp a f = 0) : CategoricalRadical.IsRadicalMorphism a

Any morphism annihilated on the right by a right-minimal morphism is categorically radical.

theorem QuotientSubmoduleEquidistribution.Iyama.isRadicalMorphism_of_comp_eq_zero_of_isLeftMinimal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y W : C} {f : X ⟶ Y} {a : Y ⟶ W} (hf : IsLeftMinimal f) (ha : CategoryTheory.CategoryStruct.comp f a = 0) : CategoricalRadical.IsRadicalMorphism a

Any morphism annihilated on the left by a left-minimal morphism is categorically radical.

theorem QuotientSubmoduleEquidistribution.Iyama.mem_radicalIdeal_of_biproduct_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J K : Type w} [Fintype J] [Fintype K] {X : J → C} {Y : K → C} (q : ⨁ X ⟶ ⨁ Y) (hq : ∀ (i : J) (j : K), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i) (CategoryTheory.CategoryStruct.comp q (CategoryTheory.Limits.biproduct.π Y j)) ∈ R.ideal.hom (X i) (Y j)) : q ∈ R.ideal.hom (⨁ X) (⨁ Y)

A matrix whose every component belongs to the chosen radical Hom ideal belongs to that ideal.

theorem QuotientSubmoduleEquidistribution.Iyama.mem_radicalIdeal_of_biproduct_source_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J : Type w} [Fintype J] {X : J → C} {Y : C} (q : ⨁ X ⟶ Y) (hq : ∀ (i : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X i) q ∈ R.ideal.hom (X i) Y) : q ∈ R.ideal.hom (⨁ X) Y

A morphism out of a finite biproduct belongs to the radical ideal when each restriction to a summand does.

theorem QuotientSubmoduleEquidistribution.Iyama.isRightMinimal_biproduct_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J : Type w} [Fintype J] {X Y : J → C} (f : (j : J) → X j ⟶ Y j) (hf : ∀ (j : J), IsRightMinimal (f j)) : IsRightMinimal (CategoryTheory.Limits.biproduct.map f)

Finite componentwise biproducts preserve right-minimal morphisms whenever the categorical radical is realized by a two-sided additive Hom ideal.

theorem QuotientSubmoduleEquidistribution.Iyama.isLeftMinimal_biproduct_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J : Type w} [Fintype J] {X Y : J → C} (f : (j : J) → X j ⟶ Y j) (hf : ∀ (j : J), IsLeftMinimal (f j)) : IsLeftMinimal (CategoryTheory.Limits.biproduct.map f)

Finite componentwise biproducts preserve left-minimal morphisms whenever the categorical radical is realized by a two-sided additive Hom ideal.

theorem QuotientSubmoduleEquidistribution.Iyama.rightTauSequence_shortComplexBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) (hS : ∀ (j : J), RightTauSequence (S j)) : RightTauSequence (shortComplexBiproduct S)

Right tau-sequences are closed under finite componentwise biproducts.

theorem QuotientSubmoduleEquidistribution.Iyama.leftTauSequence_shortComplexBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {J : Type w} [Fintype J] (S : J → CategoryTheory.ShortComplex C) (hS : ∀ (j : J), LeftTauSequence (S j)) : LeftTauSequence (shortComplexBiproduct S)

Left tau-sequences are closed under finite componentwise biproducts.