Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormAuslander

The Auslander category of the standard-form mesh #

The global-dimension and projective-injective-resolution results for the standard mesh are assembled here into the Auslander--Bongartz--Gabriel kernel equivalence.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAuslanderQuiver {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.standardFormAuslanderArrowFintype {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
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAuslanderBongartzGabrielEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      CategoryTheory.Preadditive.LeftFreyd (CategoryTheory.ProjectiveInjectiveObject S.StandardFormFiniteContravariantModuleCategory) ≌ CategoryTheory.ProjectiveObject S.StandardFormFiniteContravariantModuleCategory

      The standard mesh is an Auslander category: the left Freyd category of its projective-injective objects is equivalent to its projective objects.

      Instances For