English
Given an equivalence e between abelian groups, one obtains a canonical linear equivalence between the underlying modules after transporting the module structure along e; that is, if α ≃ β, then α ≃ₗ[R] β when α is endowed with the module structure transported from β via e.
Русский
Для эквивалентности между абелевыми группами имеется каноническое линейное эквивиправление между соответствующими модулями после переноса модуля по этой эквиви; то есть если α ≃ β, то α ≃ₗ[R] β, когда α наделён модульной структурой, переносимой от β через e.
LaTeX
$$$\\exists \\text{ transported module on } \\alpha,\\; \\alpha \\simeq_{\\text{lin}}_R \\beta$$$
Lean4
/-- An equivalence `e : α ≃ β` gives a linear equivalence `α ≃ₗ[R] β`
where the `R`-module structure on `α` is
the one obtained by transporting an `R`-module structure on `β` back along `e`.
-/
def linearEquiv (e : α ≃ β) [AddCommMonoid β] [Module R β] :
by
let addCommMonoid := Equiv.addCommMonoid e
let module := Equiv.module R e
exact α ≃ₗ[R] β := by
intros
exact
{ Equiv.addEquiv e with
map_smul' := fun r x => by
apply e.symm.injective
simp only [toFun_as_coe, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]
exact Iff.mpr (apply_eq_iff_eq_symm_apply _) rfl }
