All-module Morita equivalence to a canonical basic algebra

The finitely generated basic-projective generator already used by the representation-finite development is also a generator of the category of all modules. Applying the projective-generator Morita theorem to the contragredient skeleton gives a Morita equivalence from the original algebra to the opposite of the contragredient basic endomorphism algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientBasicProjectiveGenerator_regular_finiteAddClosure {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.finiteAddClosure S.contragredientSkeleton.basicProjectiveGenerator.obj (ModuleCat.of Aᵐᵒᵖᵐᵒᵖ Aᵐᵒᵖᵐᵒᵖ)

The regular left A-module belongs, in the category of all modules, to the finite additive closure of the basic projective generator selected by the contragredient skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.allModuleMoritaEquivalenceToContragredientBasicOpposite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : MoritaEquivalence k A S.contragredientSkeleton.moritaBasicAlgebraᵐᵒᵖ

The all-module Morita equivalence obtained from the contragredient basic projective generator. The double opposite on the source and the passage from finitely generated to all-module endomorphisms are both explicit algebra equivalences.