Iyama tau-sequences: categorical base layer

This file packages the weak-kernel, weak-cokernel, minimality, and radical approximation conditions in the definition of a right or left tau-sequence. It is independent of any module category or concrete quiver.

Mathlib represents a weak kernel by the data of an IsWeakLimit. We wrap that data in Nonempty to obtain a proposition. A weak cokernel is defined by applying the same construction in the opposite category.

def QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex D) : Prop

The first map of S exhibits a weak kernel of its second map.

def QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakCokernel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex D) : Prop

The second map of S exhibits a weak cokernel of its first map.

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.isWeakKernel_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex D) : IsWeakKernel S ↔ ∀ {W : D} (k : W ⟶ S.X₂), CategoryTheory.CategoryStruct.comp k S.g = 0 → ∃ (l : W ⟶ S.X₁), CategoryTheory.CategoryStruct.comp l S.f = k

Factorization form of the weak-kernel condition.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel.lift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex D} (hS : IsWeakKernel S) {W : D} (k : W ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) : W ⟶ S.X₁

A chosen weak-kernel factorization. Its value is noncanonical.

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel.lift_f {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex D} (hS : IsWeakKernel S) {W : D} (k : W ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) : CategoryTheory.CategoryStruct.comp (hS.lift k hk) S.f = k

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel.lift_f_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex D} (hS : IsWeakKernel S) {W : D} (k : W ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) {Z : D} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (hS.lift k hk) (CategoryTheory.CategoryStruct.comp S.f h) = CategoryTheory.CategoryStruct.comp k h

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel.exact_postcomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex D} (hS : IsWeakKernel S) (W : D) : Function.Exact (fun (l : W ⟶ S.X₁) => CategoryTheory.CategoryStruct.comp l S.f) fun (k : W ⟶ S.X₂) => CategoryTheory.CategoryStruct.comp k S.g

Evaluating a weak kernel against any source object gives an exact pair of postcomposition maps.

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.isWeakCokernel_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex D) : IsWeakCokernel S ↔ ∀ {W : D} (k : S.X₂ ⟶ W), CategoryTheory.CategoryStruct.comp S.f k = 0 → ∃ (l : S.X₃ ⟶ W), CategoryTheory.CategoryStruct.comp S.g l = k

Factorization form of the weak-cokernel condition, transported back from the opposite category.

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel.of_iso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] {S T : CategoryTheory.ShortComplex D} (hS : IsWeakKernel S) (e : S ≅ T) : IsWeakKernel T

The weak-kernel predicate is preserved by isomorphisms of short complexes.

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakCokernel.of_iso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] {S T : CategoryTheory.ShortComplex D} (hS : IsWeakCokernel S) (e : S ≅ T) : IsWeakCokernel T

The weak-cokernel predicate is preserved by isomorphisms of short complexes.

theorem QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakCokernel.exact_precomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex D} (hS : IsWeakCokernel S) (W : D) : Function.Exact (fun (l : S.X₃ ⟶ W) => CategoryTheory.CategoryStruct.comp S.g l) fun (k : S.X₂ ⟶ W) => CategoryTheory.CategoryStruct.comp S.f k

Evaluating a weak cokernel against any target object gives an exact pair of precomposition maps.

def QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsMinimalWeakKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) : Prop

A minimal weak kernel is weakly universal and right minimal.

In the intended Krull--Schmidt/Fitting setting this is equivalent to Iyama's literal condition that no nonzero summand W ⟶ 0 splits off.

def QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsMinimalWeakCokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) : Prop

A minimal weak cokernel is weakly universal and left minimal.

In the intended Krull--Schmidt/Fitting setting this is equivalent to Iyama's literal condition that no nonzero summand 0 ⟶ W splits off.

structure QuotientSubmoduleEquidistribution.Iyama.TauApproximation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) : Prop

Iyama's radical approximation condition for a complex X₁ → X₂ → X₃.

Every radical map out of X₁ factors through the first map, and every radical map into X₃ factors through the second map.

• f_radical : CategoricalRadical.IsRadicalMorphism S.f
• g_radical : CategoricalRadical.IsRadicalMorphism S.g
• factors_from_left {W : C} (a : S.X₁ ⟶ W) : CategoricalRadical.IsRadicalMorphism a → ∃ (b : S.X₂ ⟶ W), CategoryTheory.CategoryStruct.comp S.f b = a
• factors_into_right {W : C} (a : W ⟶ S.X₃) : CategoricalRadical.IsRadicalMorphism a → ∃ (b : W ⟶ S.X₂), CategoryTheory.CategoryStruct.comp b S.g = a

structure QuotientSubmoduleEquidistribution.Iyama.RightTauSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) extends QuotientSubmoduleEquidistribution.Iyama.TauApproximation S : Prop

A right tau-sequence satisfies the radical approximation condition and has a minimal weak kernel as its first map.

• f_radical : CategoricalRadical.IsRadicalMorphism S.f
• g_radical : CategoricalRadical.IsRadicalMorphism S.g
• factors_from_left {W : C} (a : S.X₁ ⟶ W) : CategoricalRadical.IsRadicalMorphism a → ∃ (b : S.X₂ ⟶ W), CategoryTheory.CategoryStruct.comp S.f b = a
• factors_into_right {W : C} (a : W ⟶ S.X₃) : CategoricalRadical.IsRadicalMorphism a → ∃ (b : W ⟶ S.X₂), CategoryTheory.CategoryStruct.comp b S.g = a
• minimalWeakKernel : ShortComplex.IsMinimalWeakKernel S

structure QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) extends QuotientSubmoduleEquidistribution.Iyama.TauApproximation S : Prop

A left tau-sequence satisfies the radical approximation condition and has a minimal weak cokernel as its second map.

• f_radical : CategoricalRadical.IsRadicalMorphism S.f
• g_radical : CategoricalRadical.IsRadicalMorphism S.g
• factors_from_left {W : C} (a : S.X₁ ⟶ W) : CategoricalRadical.IsRadicalMorphism a → ∃ (b : S.X₂ ⟶ W), CategoryTheory.CategoryStruct.comp S.f b = a
• factors_into_right {W : C} (a : W ⟶ S.X₃) : CategoricalRadical.IsRadicalMorphism a → ∃ (b : W ⟶ S.X₂), CategoryTheory.CategoryStruct.comp b S.g = a
• minimalWeakCokernel : ShortComplex.IsMinimalWeakCokernel S

theorem QuotientSubmoduleEquidistribution.Iyama.TauApproximation.f_radical_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S T : CategoryTheory.ShortComplex C} (hS : TauApproximation S) (e : S ≅ T) : CategoricalRadical.IsRadicalMorphism T.f

The first map of a tau-approximation remains radical after transporting the short complex along an isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.TauApproximation.g_radical_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S T : CategoryTheory.ShortComplex C} (hS : TauApproximation S) (e : S ≅ T) : CategoricalRadical.IsRadicalMorphism T.g

The second map of a tau-approximation remains radical after transporting the short complex along an isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.RightTauSequence.not_isZero_X₂_of_not_isZero_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (hleft : ¬CategoryTheory.Limits.IsZero S.X₁) : ¬CategoryTheory.Limits.IsZero S.X₂

If the left term of a right tau-sequence is nonzero, then its middle term is nonzero. In fact, only right minimality of the first map is used.

theorem QuotientSubmoduleEquidistribution.Iyama.RightTauSequence.isRightMinimal_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) : IsRightMinimal S.g

In a right tau-sequence, the second map is automatically right minimal. The weak-kernel and radical conditions rule out a redundant middle-term summand.

theorem QuotientSubmoduleEquidistribution.Iyama.RightTauSequence.nonempty_iso_of_iso_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S T : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (hT : RightTauSequence T) (e₃ : S.X₃ ≅ T.X₃) : Nonempty (S ≅ T)

Two right tau-sequences with isomorphic right endpoints are isomorphic as short complexes.

theorem QuotientSubmoduleEquidistribution.Iyama.RightTauSequence.exact_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (W : C) : Function.Exact (fun (l : W ⟶ S.X₁) => CategoryTheory.CategoryStruct.comp l S.f) fun (k : W ⟶ S.X₂) => CategoryTheory.CategoryStruct.comp k S.g

The contravariant representable complex of a right tau-sequence is exact at its middle term.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence.isLeftMinimal_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) : IsLeftMinimal S.f

In a left tau-sequence, the first map is automatically left minimal. The weak-cokernel and radical conditions rule out a redundant middle-term summand.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence.nonempty_iso_of_iso_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S T : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) (hT : LeftTauSequence T) (e₁ : S.X₁ ≅ T.X₁) : Nonempty (S ≅ T)

Two left tau-sequences with isomorphic left endpoints are isomorphic as short complexes.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence.exact_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) (W : C) : Function.Exact (fun (l : S.X₃ ⟶ W) => CategoryTheory.CategoryStruct.comp S.g l) fun (k : S.X₂ ⟶ W) => CategoryTheory.CategoryStruct.comp S.f k

The covariant representable complex of a left tau-sequence is exact at its middle term.