Algebra coordinates for selected primitive projectives

A complete primitive-projective presentation identifies every selected projective with a principal right ideal. Evaluation at its idempotent generator then turns a morphism between selected projectives into its literal corner element of the ambient algebra.

These coordinates reverse categorical composition: if f is followed by g, the coordinate of f ≫ g is the coordinate of g times the coordinate of f. Recording this variance once is the bridge needed to translate the Skowroński--Waschbüsch corner calculations into the right-module convention.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomTransport {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : rightIdealFGObj (P.idempotent p) ⟶ rightIdealFGObj (P.idempotent q)

Transport a selected-projective morphism to the literal principal right ideals supplied by the primitive-projective presentation.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomTransport_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q r : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) (g : S.ordinaryProjectiveObj q ⟶ S.ordinaryProjectiveObj r) : P.projectiveHomTransport (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (P.projectiveHomTransport f) (P.projectiveHomTransport g)

Transport respects composition between the literal principal right ideals.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : (S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) ≃ₗ[k] ↥(idempotentCoordinate (P.idempotent p) (rightIdealFGObj (P.idempotent q)))

The linear coordinate equivalence from a selected-projective Hom-space to the corresponding literal corner e_q A e_p. The codomain is kept in Mathlib's nested right-ideal/idempotent-coordinate form so both corner support conditions remain part of the type.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : A

The ambient algebra element representing a selected-projective morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : Function.Injective fun (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) => P.projectiveHomCoordinate f

Equality of algebra coordinates reflects equality of selected-projective morphisms.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : P.projectiveHomCoordinate 0 = 0

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_add {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f g : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : P.projectiveHomCoordinate (f + g) = P.projectiveHomCoordinate f + P.projectiveHomCoordinate g

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_neg {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : P.projectiveHomCoordinate (-f) = -P.projectiveHomCoordinate f

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_smul {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (c : k) (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : P.projectiveHomCoordinate (c • f) = c • P.projectiveHomCoordinate f

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_id {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : P.projectiveHomCoordinate (CategoryTheory.CategoryStruct.id (S.ordinaryProjectiveObj p)) = P.idempotent p

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_eq_zero_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : P.projectiveHomCoordinate f = 0 ↔ f = 0

A selected-projective morphism vanishes exactly when its literal algebra coordinate vanishes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.idempotent_mul_projectiveHomCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : P.idempotent q * P.projectiveHomCoordinate f = P.projectiveHomCoordinate f

The left corner idempotent fixes the coordinate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_mul_idempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) : P.projectiveHomCoordinate f * P.idempotent p = P.projectiveHomCoordinate f

The right corner idempotent fixes the coordinate.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomOfCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (z : A) (hleft : P.idempotent q * z = z) (hright : z * P.idempotent p = z) : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q

Turn an algebra element with the two required corner support identities back into a selected-projective morphism.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_projectiveHomOfCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (z : A) (hleft : P.idempotent q * z = z) (hright : z * P.idempotent p = z) : P.projectiveHomCoordinate (P.projectiveHomOfCoordinate z hleft hright) = z

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q r : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj p ⟶ S.ordinaryProjectiveObj q) (g : S.ordinaryProjectiveObj q ⟶ S.ordinaryProjectiveObj r) : P.projectiveHomCoordinate (CategoryTheory.CategoryStruct.comp f g) = P.projectiveHomCoordinate g * P.projectiveHomCoordinate f

Categorical composition is multiplication in reverse order in the literal right-ideal coordinates.