The basic algebra of a complete primitive-projective presentation

For a complete family of primitive idempotents in A, the finite category algebra formed from covariant representables of the selected right projectives is canonically Aᵐᵒᵖ. The opposite is forced by variance: covariant Yoneda is defined on the opposite of the projective category.

The matrix calculation is carried out on the original small selected- projective category. Its category algebra is then transported to the universe-lifted copy used by the ordinary-quiver presentation.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : Fintype S.ProjectiveCategory

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (X : S.ProjectiveCategory) : S.ProjectiveLabel

Forget the induced-category type synonym on a selected projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryLabel_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : Function.Injective projectiveCategoryLabel

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategory_finiteRepresentables {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {S : FiniteIndecomposableSkeleton k A} (X : S.ProjectiveCategory) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

Covariant representables of the small selected-projective category are finite-dimensional and finitely supported.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveToLifted {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : CategoryTheory.Functor S.ProjectiveCategory S.LiftedProjectiveCategory

Lift a selected projective and its morphisms to the universe-local copy used by the ordinary-quiver presentation.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveToLifted_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : projectiveToLifted.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveToLifted_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : CategoryTheory.Functor.Linear k projectiveToLifted

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveToLifted_full {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : projectiveToLifted.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveToLifted_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : projectiveToLifted.Faithful

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveToLifted_obj_bijective {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : Function.Bijective projectiveToLifted.obj

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveToLifted_essSurj {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : projectiveToLifted.EssSurj

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveLiftedEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : S.ProjectiveCategory ≌ S.LiftedProjectiveCategory

The small and lifted selected-projective categories are linearly equivalent by literal object reindexing.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveLiftedEquivalence_functor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : projectiveLiftedEquivalence.functor.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveLiftedEquivalence_functor_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} : CategoryTheory.Functor.Linear k projectiveLiftedEquivalence.functor

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCategoryAlgebraEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {S : FiniteIndecomposableSkeleton k A} : CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯ ≃ₐ[k] S.basicAlgebra

Objectwise universe lifting identifies the small and lifted selected- projective category algebras.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveComponent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (a : A) (X Y : S.ProjectiveCategory) : Y ⟶ X

The selected-projective morphism represented by the two-sided idempotent component e_X a e_Y.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_projectiveComponent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (a : A) (X Y : S.ProjectiveCategory) : P.projectiveHomCoordinate (P.projectiveComponent a X Y) = P.idempotent (projectiveCategoryLabel X) * a * P.idempotent (projectiveCategoryLabel Y)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.basicAlgebraAlgEquiv {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.basicAlgebra

The category algebra used by the lifted ordinary-quiver presentation is canonically the opposite of the ambient right-module algebra.