Hom vanishing into an almost-split kernel kills extensions

theorem MagnitudeConjecture.CategoryTheory.splitEpi_of_hom_to_almostSplit_kernel_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S T : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hT : T.ShortExact) (hTg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit T.g) (e : S.X₃ ≅ T.X₃) (hHom : ∀ (f : S.X₁ ⟶ T.X₁), f = 0) : CategoryTheory.IsSplitEpi S.g

A short exact sequence splits if its kernel has no maps to the kernel of a right almost-split sequence with the same endpoint.

theorem MagnitudeConjecture.CategoryTheory.extOne_eq_zero_of_hom_to_almostSplit_kernel_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] [CategoryTheory.EnoughProjectives C] {T : CategoryTheory.ShortComplex C} (hT : T.ShortExact) (hTg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit T.g) (K : C) (hHom : ∀ (f : K ⟶ T.X₁), f = 0) (xi : CategoryTheory.Abelian.Ext T.X₃ K 1) : xi = 0

The Hom-vanishing consequence of AR duality follows directly from the factorization property and realization of degree-one extensions.

theorem MagnitudeConjecture.CategoryTheory.hom_lift_of_extOne_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Q : C) (hExt : ∀ (xi : CategoryTheory.Abelian.Ext Q S.X₁ 1), xi = 0) (f : Q ⟶ S.X₃) : ∃ (g : Q ⟶ S.X₂), CategoryTheory.CategoryStruct.comp g S.g = f

Ext vanishing lifts every map through the epimorphism of a short exact sequence.