of_algEquiv — Mathlib

English

There exists a Morita equivalence between A and B whenever there is an R-algebra isomorphism between A and B.

Русский

Существование изоморфизма R-алгебр между A и B означает Морита эквивалентность между A и B.

LaTeX

$$$ (f : A \simeq_R B) \Rightarrow \text{IsMoritaEquivalent}(R,A,B)$$$

Lean4

theorem of_algEquiv {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B] (f : A ≃ₐ[R] B) :
    IsMoritaEquivalent R A B where cond := ⟨.ofAlgEquiv f⟩

Похожие утверждения