English
If e transports the R-algebra structure along an equivalence, then the base algebra map matches the transported one via the inverse equivalence.
Русский
Если перенос структуры R-алгебры вдоль эквививалентности согласуется, то базисное отображение алгебры совпадает с переносной структурой через обратное эквивалентное отображение.
LaTeX
$$$\\\\text{transported map equals inverse-transported map: } \\\\text{algebraMap}(R,\\\\alpha) = e^{-1} \\\\circ \\\\text{algebraMap}(R,\\\\beta) \\\\circ e.$$$
Lean4
theorem algebraMap_def (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) :
(@algebraMap R α _ (Equiv.semiring e) (Equiv.algebra R e)) r = e.symm ((algebraMap R β) r) :=
by
let _ := Equiv.semiring e
simp only [Algebra.algebraMap_eq_smul_one]
change e.symm (r • e 1) = e.symm (r • 1)
simp only [Equiv.one_def, apply_symm_apply]
