Coordinates of a generated submodule at a scalar corner

theorem MagnitudeConjecture.ScalarCorner.smul_mem_of_mem_span {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {M : Type w} [AddCommGroup M] [Module R M] [Module k M] [IsScalarTower k R M] (p : R) (W : Submodule k M) (hfix : ∀ x ∈ W, p • x = x) (hcorner : ∀ (a : R), ∃ (c : k), p * a * p = (algebraMap k R) c * p) {x : M} (hx : x ∈ Submodule.span R ↑W) : p • x ∈ W

Multiplying a generated relation back into the corner stays in the original vector-space relation subspace.

theorem MagnitudeConjecture.ScalarCorner.mem_span_and_fixed_iff {k : Type u} [Field k] {R : Type v} [Ring R] [Algebra k R] {M : Type w} [AddCommGroup M] [Module R M] [Module k M] [IsScalarTower k R M] (p : R) (W : Submodule k M) (hfix : ∀ x ∈ W, p • x = x) (hcorner : ∀ (a : R), ∃ (c : k), p * a * p = (algebraMap k R) c * p) (x : M) : x ∈ Submodule.span R ↑W ∧ p • x = x ↔ x ∈ W

The p-fixed vectors in the generated module are exactly the original relations, viewed inside the ambient module.