mapAlgEquiv_trans — Mathlib

English

For algebra equivalences e: A1 ≃ₐ[R] A2 and f: A2 ≃ₐ[R] A3, the map on mv-polynomials respects composition, i.e., (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f).

Русский

Для алгебраических эквивалентностей e: A1 ≃ₐ[R] A2 и f: A2 ≃ₐ[R] A3 отображение mv-многочленов сохраняет композицию, то есть (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f).

LaTeX

$$$$ (mapAlgEquiv \\; σ\\; e).trans (mapAlgEquiv \\; σ\\; f) = mapAlgEquiv \\; σ\\; (e.trans f). $$$$

Lean4

@[simp]
theorem mapAlgEquiv_trans (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) :
    (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f) :=
  by
  ext
  simp only [AlgEquiv.trans_apply, mapAlgEquiv_apply, map_map]
  rfl

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