tensorModelOfHasCoeffsInv — Mathlib

English

For any x ∈ MvPolynomial ι R0, the image under tensorModelOfHasCoeffsInv of aeval x equals 1 ⊗ quotient(x).

Русский

Для любого x ∈ MvPolynomial ι R0 образ under aeval через tensorModelOfHasCoeffsInv равен 1 ⊗ образ(x).

LaTeX

$$$P\\.tensorModelOfHasCoeffsInv\\,R_0\\ (\\mathrm{MvPolynomial}.aeval\\ P.val\\ x) = 1 \\otimes_{R_0} (\\mathrm{Ideal.Quotient.mk}\\ _\\ x)$$$

Lean4

/-- (Implementation detail): The inverse of `tensorModelOfHasCoeffsHom`. -/
noncomputable def tensorModelOfHasCoeffsInv : S →ₐ[R] R ⊗[R₀] P.ModelOfHasCoeffs R₀ :=
  (Ideal.Quotient.liftₐ _
          ((Algebra.TensorProduct.map (.id R R) (Ideal.Quotient.mkₐ _ _)).comp
            (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm.toAlgHom) <|
        by
        simp_rw [← RingHom.mem_ker, ← SetLike.le_def]
        rw [← P.span_range_relation_eq_ker, Ideal.span_le]
        rintro a ⟨i, rfl⟩
        simp only [AlgEquiv.toAlgHom_eq_coe, SetLike.mem_coe, RingHom.mem_ker, AlgHom.coe_comp, AlgHom.coe_coe,
          Function.comp_apply, algebraTensorAlgEquiv_symm_relation]
        simp only [TensorProduct.map_tmul, AlgHom.coe_id, id_eq, Ideal.Quotient.mkₐ_eq_mk, Ideal.Quotient.mk_span_range,
          tmul_zero]).comp
    (P.quotientEquiv.restrictScalars R).symm.toAlgHom

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