Endomorphism dimension drops under nonsplit extension

This file formalizes the dimension comparison used in Ringel Section 2.3, Lemma 1. Exactness bounds Hom dimensions for the middle term by those for the two endpoints. If the extension is nonsplit, one of these bounds is strict, hence replacing the endpoints by the middle term strictly lowers the endomorphism dimension, even in the presence of an unchanged direct summand.

theorem MagnitudeConjecture.LinearMap.finrank_le_add_of_exact {k : Type u} [Field k] {U V W : Type v} [AddCommGroup U] [AddCommGroup V] [AddCommGroup W] [Module k U] [Module k V] [Module k W] [FiniteDimensional k U] [FiniteDimensional k V] [FiniteDimensional k W] (f : U →ₗ[k] V) (g : V →ₗ[k] W) (hfg : Function.Exact ⇑f ⇑g) : Module.finrank k V ≤ Module.finrank k U + Module.finrank k W

Exactness at the middle term gives the elementary dimension bound dim V ≤ dim U + dim W.

theorem MagnitudeConjecture.LinearMap.finrank_lt_add_of_exact_of_not_surjective {k : Type u} [Field k] {U V W : Type v} [AddCommGroup U] [AddCommGroup V] [AddCommGroup W] [Module k U] [Module k V] [Module k W] [FiniteDimensional k U] [FiniteDimensional k V] [FiniteDimensional k W] (f : U →ₗ[k] V) (g : V →ₗ[k] W) (hfg : Function.Exact ⇑f ⇑g) (hg : ¬Function.Surjective ⇑g) : Module.finrank k V < Module.finrank k U + Module.finrank k W

If the second map in an exact pair is not onto, the middle dimension bound is strict.

theorem MagnitudeConjecture.LinearMap.finrank_eq_add_of_exact_of_injective_of_surjective {k : Type u} [Field k] {U V W : Type v} [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) (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Module.finrank k V = Module.finrank k U + Module.finrank k W

A short exact pair of linear maps gives additivity of finite dimensions.

noncomputable def MagnitudeConjecture.CategoryTheory.biproductIsoPairComplement {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type u_1} [Fintype J] [DecidableEq J] (F : J → C) (i j : J) (hij : i ≠ j) : ⨁ F ≅ (F i ⊞ F j) ⊞ ⨁ fun (t : { t : J // t ≠ i ∧ t ≠ j }) => F ↑t

Reorganize a finite biproduct by displaying two distinct summands first and collecting all remaining summands in a complementary biproduct.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.rightComp_exact {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (W : C) : Function.Exact ⇑(CategoryTheory.Linear.rightComp k W S.f) ⇑(CategoryTheory.Linear.rightComp k W S.g)

Composition out of a fixed object carries a short exact sequence to an exact pair of linear maps on Hom spaces.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.leftComp_exact {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (W : C) : Function.Exact ⇑(CategoryTheory.Linear.leftComp k W S.g) ⇑(CategoryTheory.Linear.leftComp k W S.f)

Composition into a fixed object carries a short exact sequence to the contravariant exact pair of linear maps on Hom spaces.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.finrank_hom_from_middle_le {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Balanced C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (W : C) : Module.finrank k (S.X₂ ⟶ W) ≤ Module.finrank k (S.X₃ ⟶ W) + Module.finrank k (S.X₁ ⟶ W)

Hom out of the middle term is no larger than Hom out of the direct sum of the two endpoints.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.finrank_hom_to_middle_le {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Balanced C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (W : C) : Module.finrank k (W ⟶ S.X₂) ≤ Module.finrank k (W ⟶ S.X₁) + Module.finrank k (W ⟶ S.X₃)

Hom into the middle term is no larger than Hom into the direct sum of the two endpoints.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.finrank_hom_middle_to_source_lt {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Balanced C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hnonsplit : ¬CategoryTheory.IsSplitMono S.f) : Module.finrank k (S.X₂ ⟶ S.X₁) < Module.finrank k (S.X₃ ⟶ S.X₁) + Module.finrank k (S.X₁ ⟶ S.X₁)

For a nonsplit short exact sequence, the Hom bound into the source is strict: the identity of the source cannot extend across the monomorphism.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.finrank_end_middle_lt_endpoint_blocks {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Balanced C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hnonsplit : ¬CategoryTheory.IsSplitMono S.f) : Module.finrank k (S.X₂ ⟶ S.X₂) < Module.finrank k (S.X₁ ⟶ S.X₁) + Module.finrank k (S.X₁ ⟶ S.X₃) + Module.finrank k (S.X₃ ⟶ S.X₁) + Module.finrank k (S.X₃ ⟶ S.X₃)

Ringel's strict comparison: the middle term of a nonsplit extension has smaller endomorphism dimension than the direct sum of its endpoints, written as the sum of the four matrix-block dimensions.

theorem MagnitudeConjecture.CategoryTheory.finrank_end_biprod {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (X Y : C) : Module.finrank k (X ⊞ Y ⟶ X ⊞ Y) = Module.finrank k (X ⟶ X) + Module.finrank k (X ⟶ Y) + Module.finrank k (Y ⟶ X) + Module.finrank k (Y ⟶ Y)

Endomorphisms of a binary biproduct are the four Hom matrix blocks.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.finrank_end_middle_biprod_lt {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Balanced C] [CategoryTheory.Limits.HasBinaryBiproducts C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hnonsplit : ¬CategoryTheory.IsSplitMono S.f) (R : C) : Module.finrank k (S.X₂ ⊞ R ⟶ S.X₂ ⊞ R) < Module.finrank k ((S.X₁ ⊞ S.X₃) ⊞ R ⟶ (S.X₁ ⊞ S.X₃) ⊞ R)

Ringel Section 2.3, Lemma 1 in the form needed for the minimization argument: replacing two summands by a nonsplit extension strictly lowers the endomorphism dimension even after adjoining an arbitrary unchanged summand.