algebraTensorAlgEquiv_symm_comp_aeval

English

Similar identity as above, expressing equality of composed maps via aevaluation and restriction.

Русский

Аналогично, тождество составных отображений через aevaluation и ограничение.

LaTeX

$$(( (algebraTensorAlgEquiv (σ := σ) R A).symm.restrictScalars R) ∘ (MvPolynomial.mapAlgHom (R := R) (S₁ := R) (S₂ := A) (Algebra.ofId R A))) = Algebra.TensorProduct.includeRight$$

Lean4

@[simp]
theorem algebraTensorAlgEquiv_symm_comp_aeval :
    (((algebraTensorAlgEquiv (σ := σ) R A).symm.restrictScalars R) :
            MvPolynomial σ A →ₐ[R] A ⊗[R] MvPolynomial σ R).comp
        (MvPolynomial.mapAlgHom (R := R) (S₁ := R) (S₂ := A) (Algebra.ofId R A)) =
      Algebra.TensorProduct.includeRight :=
  by
  ext
  simp

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