Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormAuslanderProjective

Projective-injective copresentations of projective standard-mesh modules #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAuslanderProjectiveQuiver {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.standardFormAuslanderProjectiveArrowFintype {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.standardFormProjective_projectiveInjectiveCopresentation_nonempty {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (P : CategoryTheory.ProjectiveObject S.StandardFormFiniteContravariantModuleCategory) :
      Nonempty (CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation P.obj)

      Every projective finite module on the standard mesh has a two-term projective-injective copresentation.