The primitive corner is scalar in a directed module category #
theorem
MagnitudeConjecture.RightModule.corner_scalar_of_rightIdeal_endomorphisms
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{e : A}
(he : IsIdempotentElem e)
(hP :
∀ (f : rightIdealFGObj e ⟶ rightIdealFGObj e),
∃ (c : k), c • CategoryTheory.CategoryStruct.id (rightIdealFGObj e) = f)
(a : A)
:
∃ (c : k), e * a * e = (algebraMap k A) c * e
Scalar endomorphisms of eA force every eae to be a scalar multiple of e.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveProjective_endomorphism_scalar
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
[IsAlgClosed k]
(H : S.HasAcyclicNonzeroNonisomorphisms)
{e : A}
(D : PrimitiveIdempotentData e)
(f : rightIdealFGObj e ⟶ rightIdealFGObj e)
:
∃ (c : k), c • CategoryTheory.CategoryStruct.id (rightIdealFGObj e) = f
Directedness supplies scalar endomorphisms on the literal primitive projective, by transport from its selected skeleton representative.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitive_opposite_corner_scalar
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
[IsAlgClosed k]
(H : S.HasAcyclicNonzeroNonisomorphisms)
{e : A}
(D : PrimitiveIdempotentData e)
(a : Aᵐᵒᵖ)
:
∃ (c : k), MulOpposite.op e * a * MulOpposite.op e = (algebraMap k Aᵐᵒᵖ) c * MulOpposite.op e
The scalar-corner condition in right-module (opposite-ring) convention.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedCoordinateRelations_coordinate_iff
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
[IsAlgClosed k]
(H : S.HasAcyclicNonzeroNonisomorphisms)
{e : A}
(D : PrimitiveIdempotentData e)
(V : FinitelyGeneratedCategory A)
(R : Submodule k ↥(idempotentCoordinate e V))
(x : ↥(idempotentCoordinate e V))
:
↑x ∈ generatedCoordinateRelations e V R ↔ x ∈ R
Coordinate membership for the generated relation module, with the scalar corner condition discharged by directedness.