Homogeneous corners under algebra equivalence

def MagnitudeConjecture.Graded.cornerComapEquiv {k : Type u_1} {A : Type u_2} {B : Type u_3} [Field k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] (R : VectorGrading k B) (E : A ≃ₐ[k] B) (e f : B) (d : ℤ) : ↥(cornerComponent (R.comap ↑E) (E.symm e) (E.symm f) d) ≃ₗ[k] ↥(cornerComponent R e f d)

Pulling a grading and two idempotents back along an algebra equivalence preserves their homogeneous corner spaces.