tensorModelOfHasCoeffsHom — Mathlib

English

The underlying AlgHom of tensorModelOfHasCoeffsEquiv is given by a lifted algebra homomorphism from the tensor product to S.

Русский

Базовая реализация tensorModelOfHasCoeffsEquiv задаётся поднимаемым алгебра-гомоморфизмом из тензорного произведения в S.

LaTeX

$$$\\text{tensorModelOfHasCoeffsHom} : R \\otimes_{R_0} P.ModelOfHasCoeffs R_0 \\to_{\\mathsf{Alg}} S$$$

Lean4

/-- (Implementation detail): The underlying `AlgHom` of `tensorModelOfHasCoeffsEquiv`. -/
noncomputable def tensorModelOfHasCoeffsHom : R ⊗[R₀] P.ModelOfHasCoeffs R₀ →ₐ[R] S :=
  Algebra.TensorProduct.lift (Algebra.ofId R S)
    (Ideal.Quotient.liftₐ _ (MvPolynomial.aeval P.val) <|
      by
      simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le]
      rintro a ⟨i, rfl⟩
      simp)
    fun _ _ ↦ Commute.all _ _

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