English
Let A and B be R-algebras that are isomorphic as R-algebras. Then A and B are Morita equivalent over R; the Morita equivalence is obtained by restricting scalars along the inverse algebra isomorphism.
Русский
Пусть A и B — R-алгебры, изоморфны как R-алгебры. Тогда A и B над R Морита эквивалентны; эквивалентность задаётся ограничением скаляров по обратному изоморфизму алгебр.
LaTeX
$$$ (A \simeq_R B) \Rightarrow \text{MoritaEquivalence}(R,A,B)$$$
Lean4
/-- Isomorphic `R`-algebras are Morita equivalent.
-/
noncomputable def ofAlgEquiv {A : Type u₁} {B : Type u₂} [Ring A] [Algebra R A] [Ring B] [Algebra R B] (f : A ≃ₐ[R] B) :
MoritaEquivalence R A B
where
eqv := ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm.toRingEquiv
linear := ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear f.symm
