Ext vanishing for modules generated at an idempotent #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOne_eq_zero_of_hom_to_rightTranslation_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)]
(S : FiniteIndecomposableSkeleton k A)
(z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) })
(K : FinitelyGeneratedCategory A)
(hHom : ∀ (f : K ⟶ S.fgObj (S.rightTranslationLabel z)), f = 0)
(xi : CategoryTheory.Abelian.Ext (S.fgObj ↑z) K 1)
:
xi = 0
Hom vanishing into the translate annihilates extensions out of its nonprojective endpoint. No directedness hypothesis is needed.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOne_eq_zero_of_generated_at_idempotent
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)]
(S : FiniteIndecomposableSkeleton k A)
{e : A}
(he : IsIdempotentElem e)
(z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) })
(K : FinitelyGeneratedCategory A)
(hK : IsGeneratedAtIdempotent e K)
(htau : ∀ (y : ↑(S.fgObj (S.rightTranslationLabel z))), MulOpposite.op e • y = 0)
(xi : CategoryTheory.Abelian.Ext (S.fgObj ↑z) K 1)
:
xi = 0
A module generated at e has no extensions from a nonprojective module whose AR translate is killed by e.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedCoordinateRelations_extOne_eq_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)]
(S : FiniteIndecomposableSkeleton k A)
{e : A}
(he : IsIdempotentElem e)
(z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) })
(V : FinitelyGeneratedCategory A)
(R : Submodule k ↥(idempotentCoordinate e V))
(htau : ∀ (y : ↑(S.fgObj (S.rightTranslationLabel z))), MulOpposite.op e • y = 0)
(xi : CategoryTheory.Abelian.Ext (S.fgObj ↑z) (generatedCoordinateRelationsFGObj e V R) 1)
:
xi = 0
In particular, the module generated by coordinate relations satisfies this Ext vanishing.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjective_extOne_eq_zero_of_generated
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)]
(S : FiniteIndecomposableSkeleton k A)
{e : A}
(D : PrimitiveIdempotentData e)
(p : S.FactorProjectiveLabel (S.primitiveKilledLabels D))
(K : FinitelyGeneratedCategory A)
(hK : IsGeneratedAtIdempotent e K)
(xi : CategoryTheory.Abelian.Ext (S.fgObj ↑↑p) K 1)
:
xi = 0
Every tau-projective of the primitive factor has vanishing Ext into a module generated at e, including the ambient projective case.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjective_hom_lift_of_generated_kernel
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)]
(S : FiniteIndecomposableSkeleton k A)
{e : A}
(D : PrimitiveIdempotentData e)
(p : S.FactorProjectiveLabel (S.primitiveKilledLabels D))
{T : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)}
(hT : T.ShortExact)
(hK : IsGeneratedAtIdempotent e T.X₁)
(f : S.fgObj ↑↑p ⟶ T.X₃)
:
∃ (g : S.fgObj ↑↑p ⟶ T.X₂), CategoryTheory.CategoryStruct.comp g T.g = f
Maps from the primitive factor's tau-projectives lift across every short exact sequence whose kernel is generated at e.