Homogeneous maps between singleton additive-envelope objects

def MagnitudeConjecture.GradedCategory.HomGrading.additiveEmbeddingComponentEquiv {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (X Y : C) (d : ℤ) : ↥(G.additiveEnvelope.component ((CategoryTheory.Mat_.embedding C).obj X) ((CategoryTheory.Mat_.embedding C).obj Y) d) ≃ₗ[k] ↥(G.component X Y d)

The additive embedding preserves each homogeneous Hom space exactly.