Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormMeshExtVanishing

Mesh Ext vanishing in standard form #

The Hom exactness for the standard mesh-simple resolution implies the Ext¹ vanishing used in Bongartz--Gabriel Lemma 2.6(c).

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshExtFinalQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshExtFinalArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
    Fintype (x ⟶ y)
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimple_extOne_contravariantRepresentable_subsingleton {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt (CoveringHom.FiniteDimensionalModuleCategory k)] (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) (x : Fin S.n) :
      Subsingleton (CategoryTheory.Abelian.Ext (S.standardFormRightMeshData.simpleFiniteModule ↑z) (S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x) 1)

      Bongartz--Gabriel Lemma 2.6(c) for the standard-form mesh category: Ext¹ from a nonprojective mesh simple to every contravariant representable vanishes.