Splitting homogeneous idempotents of graded modules

def MagnitudeConjecture.Graded.FiniteGradedModule.imageObject {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X : FiniteGradedModule R) (f : ↑X.module →ₗ[A] ↑X.module) (hf : X.grading.Homogeneous X.grading 0 f) : FiniteGradedModule R

The image of a degree-zero endomorphism as a finite graded module.

instance MagnitudeConjecture.Graded.FiniteGradedModule.instIsIdempotentCompleteDegreeObjectHomGrading {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : CategoryTheory.IsIdempotentComplete (GradedCategory.DegreeObject homGrading)

Homogeneous idempotents split through their actual module image.