quotIdealMapEquivTensorQuot_mk — Mathlib

English

Let A and B be commutative rings with an A-algebra structure on B, and I an ideal of A. The natural quotient–tensor isomorphism sends each b ∈ B to the pure tensor b ⊗ 1 in B ⊗_A (A/I).

Русский

Пусть A и B — коммутативные кольца, задано структуру A-алгебры на B, и I — идеал A. Натуральный изоморфизм тензорного произведения через фактор-марку отправляет каждый b ∈ B в чистый тензор b ⊗ 1 в B ⊗_A (A/I).

LaTeX

$$$\\mathrm{quotIdealMapEquivTensorQuot}_{B,I}(b) = b \\otimes_A 1$$$

Lean4

@[simp]
theorem quotIdealMapEquivTensorQuot_mk (b : B) : quotIdealMapEquivTensorQuot B I b = b ⊗ₜ[A] 1 :=
  rfl

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