No extra coordinate relations are generated at a scalar corner

theorem MagnitudeConjecture.RightModule.mem_generatedCoordinateRelations_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (hcorner : ∀ (a : Aᵐᵒᵖ), ∃ (c : k), MulOpposite.op e * a * MulOpposite.op e = (algebraMap k Aᵐᵒᵖ) c * MulOpposite.op e) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) (x : ↥(idempotentCoordinate e V)) : ↑x ∈ generatedCoordinateRelations e V R ↔ x ∈ R

For a scalar corner, the e-coordinate of the generated relation module contains exactly the original vector-space relations.