algEquivIncludeRange_symm_toAlgHom

English

Let R,S,T be as above and A,B be subalgebras of S. The inverse of the natural inclusion-range isomorphism is equal to the product map on the ranges, i.e., the symmetrized form coincides with range.mulMap applied to includeLeft and includeRight.

Русский

Пусть R,S,T удовлетворяют условиям, A и B — подалгебры S. Обратное к естественному изоморфизму включения-диапазона равняется произведению на диапазонах: симметризованная форма совпадает с range.mulMap, применённой к includeLeft и includeRight.

LaTeX

$$$(\text{algEquivIncludeRange } R S T)^{-1}.toAlgHom = (\text{includeLeft} : S \to_R S \otimes_R T).range.mulMap includeRight.range$$$

Lean4

theorem algEquivIncludeRange_symm_toAlgHom :
    (algEquivIncludeRange R S T).symm.toAlgHom = (includeLeft : S →ₐ[R] S ⊗[R] T).range.mulMap includeRight.range :=
  rfl

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