Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormAuslanderRepresentable

Projective-injective copresentations of standard-mesh representables #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAuslanderRepresentableQuiver {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.standardFormAuslanderRepresentableArrowFintype {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
      @[reducible, inline]
      abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormFiniteContravariantModuleCategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      Type (u + 1)
      Instances For
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormContravariantRepresentableProjectiveInjectiveCopresentation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) :
        CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation (S.standardFormRightMeshData.contravariantRepresentableFiniteModule ⋯ x)

        The chosen injective copresentation of a standard-mesh representable has projective-injective terms.

        Instances For