English
Composition of Morita equivalences yields Morita equivalence; explicit construction via eqv and linear components.
Русский
Состав Morita-эквивалентностей образует Morita-эквивалентность; явное построение через эквивалентность и линейные компоненты.
LaTeX
$$MoritaEquivalence.trans R A B C e e' $$
Lean4
/-- For any `R`-algebras `A`, `B`, and `C`, if `A` is Morita equivalent to `B` and `B` is Morita
equivalent to `C`, then `A` is Morita equivalent to `C`.
-/
def trans {A B C : Type u₁} [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Ring C] [Algebra R C]
(e : MoritaEquivalence R A B) (e' : MoritaEquivalence R B C) : MoritaEquivalence R A C
where
eqv := e.eqv.trans e'.eqv
linear := e.eqv.functor.instLinearComp e'.eqv.functor
