sumAlgEquiv_comp_rename_inr — Mathlib

English

The sum-algebra equivalence composed with renaming on the right-injection yields the canonical scalar-tower embedding.

Русский

Комбинация суммной алгебраической эквивалентности и переименования по правой инъекции приводит к каноническому вложению-масштабу.

LaTeX

$$$ (\text{sumAlgEquiv } R S_1 S_2)\cdot(\text{rename }\mathrm{inr}) = \text{IsScalarTower.toAlgHom } R (MvPolynomial S_2 R) (MvPolynomial S_1 (MvPolynomial S_2 R))$$$

Lean4

theorem sumAlgEquiv_comp_rename_inr :
    (sumAlgEquiv R S₁ S₂).toAlgHom.comp (rename Sum.inr) =
      IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R)) :=
  by
  ext i
  simp

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