Dimension recurrence from a strict right tau-sequence

For a strict right tau-sequence X₁ ⟶ X₂ ⟶ X₃, evaluation at a source object W gives a short exact sequence

0 ⟶ Hom(W,X₁) ⟶ Hom(W,X₂) ⟶ rad(W,X₃) ⟶ 0.

This file constructs the radical as a linear subspace and proves the resulting finite-dimensional equality. It is the linear-algebraic heart of the mesh/ Hom inverse recurrence.

def MagnitudeConjecture.CategoryTheory.radicalSubmodule (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) : Submodule k (X ⟶ Y)

The categorical radical between two objects, as a linear subspace of the Hom space.

def MagnitudeConjecture.CategoryTheory.rightCompToRadical (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : C) {Y Z : C} (g : Y ⟶ Z) (hg : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism g) : (W ⟶ Y) →ₗ[k] ↥(radicalSubmodule k W Z)

Postcomposition by a radical morphism, with codomain restricted to the radical subspace.

def MagnitudeConjecture.CategoryTheory.radicalTargetLinearEquiv (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) {Y Z : C} (e : Y ≅ Z) : ↥(radicalSubmodule k X Y) ≃ₗ[k] ↥(radicalSubmodule k X Z)

Postcomposition by an isomorphism transports the radical subspace.

def MagnitudeConjecture.CategoryTheory.radicalSourceLinearEquiv (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X Z : C} (e : X ≅ Z) : ↥(radicalSubmodule k X Y) ≃ₗ[k] ↥(radicalSubmodule k Z Y)

Precomposition by an isomorphism transports the radical subspace.

def MagnitudeConjecture.CategoryTheory.leftCompToRadical (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : C) {X Y : C} (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f) : (Y ⟶ W) →ₗ[k] ↥(radicalSubmodule k X W)

Precomposition by a radical morphism, with codomain restricted to the radical subspace.

theorem MagnitudeConjecture.CategoryTheory.finrank_middle_eq_add_of_exact (k : Type s) [Field k] {U : Type u_1} {V : Type u_2} {W : Type u_3} [AddCommGroup U] [AddCommGroup V] [AddCommGroup W] [Module k U] [Module k V] [Module k W] [FiniteDimensional k V] (f : U →ₗ[k] V) (g : V →ₗ[k] W) (hExact : Function.Exact ⇑f ⇑g) (f_injective : Function.Injective ⇑f) (g_surjective : Function.Surjective ⇑g) : Module.finrank k V = Module.finrank k U + Module.finrank k W

Rank-nullity form of a finite-dimensional short exact sequence of linear maps.

theorem MagnitudeConjecture.CategoryTheory.rightTauSequence_finrank (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (hS : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence S) [CategoryTheory.Mono S.f] (W : C) [FiniteDimensional k (W ⟶ S.X₂)] : Module.finrank k (W ⟶ S.X₂) = Module.finrank k (W ⟶ S.X₁) + Module.finrank k ↥(radicalSubmodule k W S.X₃)

Hom-dimension recurrence supplied by a strict right tau-sequence.

theorem MagnitudeConjecture.CategoryTheory.leftTauSequence_finrank (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (hS : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence S) [CategoryTheory.Epi S.g] (W : C) [FiniteDimensional k (S.X₂ ⟶ W)] : Module.finrank k (S.X₂ ⟶ W) = Module.finrank k (S.X₃ ⟶ W) + Module.finrank k ↥(radicalSubmodule k S.X₁ W)

Dual Hom-dimension recurrence supplied by a strict left tau-sequence.