English
An equivalence e: α ≃ β induces an R-algebra equivalence α ≃ₐ[R] β, where the R-algebra structure on α is obtained by transporting the R-algebra structure on β back along e.
Русский
Эквивелентность e: α ≃ β порождает алгебраическое эквивалентное отображение α ≃ₐ[R] β, причём структура R-алгебры на α получается путём переноса структуры β обратно вдоль e.
LaTeX
$$$\\\\text{AlgEquiv}_R(\\alpha,\\beta) \\text{ exists with underlying } e:\\alpha\\\\to\\\\beta, \\text{ transported structure on } \\alpha.$$$
Lean4
/-- Transfer `Algebra` across an `Equiv` -/
protected abbrev algebra (e : α ≃ β) [Semiring β] :
let _ := Equiv.semiring e
∀ [Algebra R β], Algebra R α :=
by
intros
letI : Module R α := e.module R
fapply Algebra.ofModule
· intro r x y
change e.symm (e (e.symm (r • e x)) * e y) = e.symm (r • e.ringEquiv (x * y))
simp only [apply_symm_apply, Algebra.smul_mul_assoc, map_mul, ringEquiv_apply]
· intro r x y
change e.symm (e x * e (e.symm (r • e y))) = e.symm (r • e (e.symm (e x * e y)))
simp only [apply_symm_apply, Algebra.mul_smul_comm]
