Transporting graded modules along algebra equivalences

def MagnitudeConjecture.Graded.restrictedScalarTower {k : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [Field k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] [AddCommGroup M] [Module k M] [Module B M] [IsScalarTower k B M] (e : A ≃ₐ[k] B) : IsScalarTower k A M

Restriction along an algebra equivalence retains the original scalar tower.

def MagnitudeConjecture.Graded.ModuleGrading.restrictAlgebra {k : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [Field k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] [AddCommGroup M] [Module k M] [Module B M] {R : VectorGrading k B} (G : ModuleGrading R) (e : A ≃ₐ[k] B) : ModuleGrading (R.comap ↑e)

The same homogeneous module components, with action restricted along the algebra equivalence.

def MagnitudeConjecture.Graded.restrictAlgebraMap {k : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [Field k] [Ring A] [Ring B] [Algebra k A] [Algebra k B] [AddCommGroup M] [Module B M] {N : Type u_5} [AddCommGroup N] [Module B N] (e : A ≃ₐ[k] B) (f : M →ₗ[B] N) : M →ₗ[A] N

Existing module maps remain linear after transport of the algebra action.