The canonical basic Morita representative

For a finite indecomposable skeleton of finitely generated right modules, let G be the biproduct of one representative of every indecomposable projective. The represented functor Hom(G, -) identifies the original finitely generated module category with the finitely generated right modules over End(G).

This file packages that elementary projective-generator Morita equivalence. It uses no structural input about special biserial or string algebras.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectiveGenerator {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FinitelyGeneratedCategory A

The biproduct of one representative of every indecomposable projective right module.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectiveGenerator_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Projective S.basicProjectiveGenerator

The chosen projective generator is projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteAddClosure_basicProjectiveGenerator_of_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) (hX : CategoryTheory.Projective X) : CategoryTheory.finiteAddClosure S.basicProjectiveGenerator X

Every finitely generated projective right module belongs to the additive closure of the chosen projective generator.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicAlgebra {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type u

The endomorphism algebra of the chosen projective generator. This is the canonical basic representative used below.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicAlgebra_finiteDimensional {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FiniteDimensional k S.moritaBasicAlgebra

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicAlgebra_opposite_noetherian {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : IsNoetherianRing S.moritaBasicAlgebraᵐᵒᵖ

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_basicProjectiveGenerator_hom_comp_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (hf : f ≠ 0) : ∃ (g : S.basicProjectiveGenerator ⟶ X), CategoryTheory.CategoryStruct.comp g f ≠ 0

Maps out of the chosen projective generator detect every nonzero map.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectiveGenerator_coyoneda_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : (CategoryTheory.preadditiveCoyonedaObj S.basicProjectiveGenerator).Faithful

The represented functor of the chosen projective generator is faithful.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectiveGeneratorPresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CategoryTheory.FiniteAddGeneratorPresentation S.basicProjectiveGenerator X

The standard kernel presentation by a projective cover, expressed in the interface used by the generic representable-fullness theorem.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectiveGenerator_coyoneda_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : (CategoryTheory.preadditiveCoyonedaObj S.basicProjectiveGenerator).Full

The represented functor of the chosen projective generator is full.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (FinitelyGeneratedCategory A) (FinitelyGeneratedCategory S.moritaBasicAlgebra)

Hom(G,-) restricted to finitely generated right modules over End(G).

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaFunctor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.basicMoritaFunctor.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaFunctor_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.basicMoritaFunctor

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaFunctor_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.basicMoritaFunctor.Faithful

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaFunctor_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.basicMoritaFunctor.Full

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectiveGeneratorPower {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (n : ℕ) : FinitelyGeneratedCategory A

A finite power of the chosen projective generator.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaGeneratorPowerIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (n : ℕ) : (CategoryTheory.preadditiveCoyonedaObj S.basicProjectiveGenerator).obj (S.basicProjectiveGeneratorPower n) ≅ ModuleCat.of S.moritaBasicAlgebraᵐᵒᵖ (Fin n → S.moritaBasicAlgebraᵐᵒᵖ)

The represented module of a finite generator power is finite free.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaFunctor_essSurj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.basicMoritaFunctor.EssSurj

Every finitely generated right module over End(G) is represented.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FinitelyGeneratedCategory A ≌ FinitelyGeneratedCategory S.moritaBasicAlgebra

The canonical Morita equivalence from the original right-module category to the right modules over the basic endomorphism algebra.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicMoritaEquivalence_functor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.basicMoritaEquivalence.functor.Additive

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

The complete indecomposable skeleton transported to the canonical basic endomorphism algebra. Labels are deliberately unchanged.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicSkeletonObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : S.basicMoritaEquivalence.functor.obj (S.fgObj i) ≅ S.moritaBasicSkeleton.fgObj i

Each object of the transported skeleton is canonically the represented module of the original object with the same label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_moritaBasicSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.moritaBasicSkeleton.ambientARSurplus = S.ambientARSurplus

Passage to the canonical basic representative preserves the ambient Auslander--Reiten surplus.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicSkeleton_beta_le {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {bound : ℕ} (h : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ bound) : FiniteTauMatrix.beta S.moritaBasicSkeleton.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ bound

Any uniform beta bound for the original skeleton passes to the canonical basic representative.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjector {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : S.moritaBasicAlgebra

The projector of the projective generator onto one indecomposable projective summand.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjector_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CompleteOrthogonalIdempotents S.basicProjector

The summand projectors form a complete orthogonal family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjector_primitive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : PrimitiveIdempotentData (S.basicProjector p)

Each summand projector is primitive.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectorRightIdealLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : ↑(rightIdealFGObj (S.basicProjector p)) ≃ₗ[S.moritaBasicAlgebraᵐᵒᵖ] ↑(S.basicMoritaFunctor.obj (S.fgObj p.label))

The principal right ideal of a summand projector is the represented module of that summand.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicProjectorRightIdealIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : rightIdealFGObj (S.basicProjector p) ≅ S.basicMoritaFunctor.obj (S.fgObj p.label)

Categorical form of the principal-right-ideal identification.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveLabel_eq_of_label_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {p q : S.ProjectiveLabel} (h : p.label = q.label) : p = q

Projective labels are determined by their underlying skeleton labels.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicProjectiveLabelEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.ProjectiveLabel ≃ S.moritaBasicSkeleton.ProjectiveLabel

The original and transported projective labels correspond label by label under the Morita equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moritaBasicPrimitiveProjectivePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.moritaBasicSkeleton.PrimitiveProjectivePresentation

The summand projectors give the transported skeleton its canonical primitive-projective presentation.