Uniqueness of finite-dimensional basic Morita representatives

A complete duplicate-free primitive-projective presentation identifies the ambient algebra with the endomorphism algebra of the sum of its distinct indecomposable projective right modules. A linear equivalence of right-module categories identifies those endomorphism algebras. These are the two pieces needed to turn Morita equivalence into algebra equivalence when both displayed representatives are basic.

def MagnitudeConjecture.RightModule.rightRegularLeftMulFGHom {A : Type u} [Ring A] (a : A) : rightRegularFGObj ⟶ rightRegularFGObj

Left multiplication by an algebra element as an endomorphism of the finitely generated regular right module.

@[simp]

theorem MagnitudeConjecture.RightModule.rightRegularLeftMulFGHom_apply {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (a x : A) : (ModuleCat.Hom.hom (rightRegularLeftMulFGHom a).hom) x = a * x

def MagnitudeConjecture.RightModule.rightRegularEndAlgEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] : A ≃ₐ[k] CategoryTheory.End rightRegularFGObj

Left multiplication identifies an algebra with the categorical endomorphism algebra of its regular right module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.regularIsoBasicProjectiveGenerator {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : rightRegularFGObj ≅ S.basicProjectiveGenerator

A complete primitive family decomposes the regular module into the chosen duplicate-free projective generator.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ambientAlgEquivMoritaBasic {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : A ≃ₐ[k] S.moritaBasicAlgebra

A basic algebra supplied with its literal primitive-projective presentation is algebra-equivalent to the canonical basic representative formed from its right-module skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mapEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (E : FGModuleCat Aᵐᵒᵖ ≌ FGModuleCat Bᵐᵒᵖ) [E.functor.Additive] [E.inverse.Additive] : FiniteIndecomposableSkeleton k B

Transport a complete duplicate-free indecomposable right-module skeleton through an additive equivalence.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mapEquivalenceObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (E : FGModuleCat Aᵐᵒᵖ ≌ FGModuleCat Bᵐᵒᵖ) [E.functor.Additive] [E.inverse.Additive] (i : Fin S.n) : E.functor.obj (S.fgObj i) ≅ (S.mapEquivalence E).fgObj i

The transported skeleton object is the functorial image of the original object with the same finite label.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mapEquivalenceProjectiveLabelEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (E : FGModuleCat Aᵐᵒᵖ ≌ FGModuleCat Bᵐᵒᵖ) [E.functor.Additive] [E.inverse.Additive] : S.ProjectiveLabel ≃ (S.mapEquivalence E).ProjectiveLabel

Projective labels are transported without changing the underlying finite label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectiveGeneratorMapIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (E : FGModuleCat Aᵐᵒᵖ ≌ FGModuleCat Bᵐᵒᵖ) [E.functor.Additive] [E.inverse.Additive] : E.functor.obj S.basicProjectiveGenerator ≅ (S.mapEquivalence E).basicProjectiveGenerator

The image of the duplicate-free projective generator is the projective generator of the transported skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicAlgebraEquivOfEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (E : FGModuleCat Aᵐᵒᵖ ≌ FGModuleCat Bᵐᵒᵖ) [E.functor.Additive] [E.inverse.Additive] [CategoryTheory.Functor.Linear k E.functor] : S.moritaBasicAlgebra ≃ₐ[k] (S.mapEquivalence E).moritaBasicAlgebra

A linear equivalence of finitely generated right-module categories identifies the canonical basic endomorphism algebras.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ambient_admitsSpecialBiserialPresentation_of_isSpecialBiserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hSpecial : BoundQuiver.IsSpecialBiserial k A) : BoundQuiver.AdmitsSpecialBiserialPresentation k A

For an algebra already certified as basic by a primitive-projective presentation, the Morita-invariant special-biserial predicate can be realized by a literal special-biserial presentation of the ambient algebra.