English
If there is a bijection between R and A via algebraMap and M is an R-module with an A-structure compatible with the tower, then a basis of M as an R-module remains a basis as an A-module after transporting coefficients along the bijection.
Русский
При существовании биекции между R и A через алгебраическое отображение и совместимости модуля, база M как R-модуля сохраняет свойство базы как A-модуля после переноса коэффициентов по биекции.
LaTeX
$$$$ \text{If } b: \text{Basis}_{ι} R M \text{ and } h \text{ bijective for algebraMap},\; b.algebraMapCoeffs A h \text{ is a Basis for } M \text{ over } A $$$$
Lean4
/-- If `R` and `A` have a bijective `algebraMap R A` and act identically on `M`,
then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module. -/
@[simps! repr_apply_toFun]
noncomputable def algebraMapCoeffs : Basis ι A M :=
b.mapCoeffs (RingEquiv.ofBijective _ h) fun c x => by simp
