English
An equivalence e yields a canonical R-algebra isomorphism between α and β, provided β has an R-algebra structure.
Русский
Эквивелентность e порождает каноническое алгебра-изоморфизм между α и β при условии, что β имеет структуру R-алгебры.
LaTeX
$$$\\\\alpha \\\\equiv_R \\\\beta \\\\cong\\\\mathrm{AlgEquiv}_R(\\\\alpha,\\\\beta) \\\\text{ с основанием } e$$$
Lean4
/-- An equivalence `e : α ≃ β` gives an algebra equivalence `α ≃ₐ[R] β`
where the `R`-algebra structure on `α` is
the one obtained by transporting an `R`-algebra structure on `β` back along `e`. -/
def algEquiv (e : α ≃ β) [Semiring β] [Algebra R β] :
by
let semiring := Equiv.semiring e
let algebra := Equiv.algebra R e
exact α ≃ₐ[R] β := by
intros
exact
{ Equiv.ringEquiv e with
commutes' := fun r => by
apply e.symm.injective
simp only [RingEquiv.toEquiv_eq_coe, toFun_as_coe, EquivLike.coe_coe, ringEquiv_apply, symm_apply_apply,
algebraMap_def] }
