English
If an R-algebra A is isomorphic to R as an R-module, then the canonical map R → A is an R-algebra isomorphism; and if e: R ≃ₗ[R] A, the isomorphism aligns with e(1)=1 when appropriate.
Русский
Если R-алгебра A изоморфна как R-модуль R, то каноническое отображение R→A является изоморфизмом R-алгебр; и если e: R ≃ₗ[R] A, этот изоморфизм согласуется с e(1)=1 при необходимости.
LaTeX
$$$ \\text{algEquivOfRing }(e: R \\simeq_{R} A): R \\simeq_{R} A. $$$
Lean4
/-- If an `R`-algebra `A` is isomorphic to `R` as `R`-module, then the canonical map `R → A` is an
equivalence of `R`-algebras.
Note that if `e : R ≃ₗ[R] A` is the linear equivalence, then this is not the same as the equivalence
of algebras provided here unless `e 1 = 1`. -/
@[simps]
def algEquivOfRing {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (e : R ≃ₗ[R] A) : R ≃ₐ[R] A
where
__ := Algebra.ofId R A
invFun x := e.symm (e 1 * x)
left_inv
x :=
calc
e.symm (e 1 * (algebraMap R A) x) = e.symm (x • e 1) := by rw [Algebra.smul_def, mul_comm]
_ = x := by rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
right_inv
x :=
calc
(algebraMap R A) (e.symm (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1) := by
rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
_ = x := by
rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1), ← map_smul, smul_eq_mul, mul_one,
e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def, ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply,
one_mul]
