Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleARHomVanishing

AR-duality vanishing from ordinary Hom vanishing #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOne_rightTranslation_subsingleton_of_hom_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (U : FinitelyGeneratedCategory A) (hHom : ∀ (f : S.fgObj ↑z ⟶ U), f = 0) :
Subsingleton (CategoryTheory.Abelian.Ext U (S.fgObj (S.rightTranslationLabel z)) 1)

Ordinary Hom vanishing suffices for Ext vanishing into the AR translate.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOne_rightTranslation_subsingleton_of_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (I : FinitelyGeneratedCategory A) (hHom : ∀ (f : S.fgObj ↑z ⟶ I), f = 0) (U : FinitelyGeneratedCategory A) (j : U ⟶ I) [CategoryTheory.Mono j] :
Subsingleton (CategoryTheory.Abelian.Ext U (S.fgObj (S.rightTranslationLabel z)) 1)

Hom vanishing into I also holds into every subobject of I, so AR duality provides precisely the subobject Ext vanishing used by the finite-kernel lemma.