tensorEquiv — Mathlib

English

Given the same setup as above, there is a canonical localization structure on A ⊗R S at the same inverted element, reflecting the symmetry of the tensor product.

Русский

При той же постановке существует каноническая структура локализации на A ⊗R S по тем же инвертируемым элементам, что и выше, отражающая симметрию тензорного произведения.

LaTeX

$$$\\operatorname{IsLocalization}\\!\\_\\mathrm{Away}\\bigl(\\mathrm{algebraMap}\\_R^S(r)\\bigr)\\bigl(A \\otimes_R S\\bigr)$$

Lean4

/-- The `S`-isomorphism `S ⊗[R] Rᵣ ≃ₐ Sᵣ`. -/
noncomputable abbrev tensorEquiv [IsLocalization.Away r A] : S ⊗[R] A ≃ₐ[S] Localization.Away (algebraMap R S r) :=
  IsLocalization.algEquiv (Submonoid.powers <| algebraMap R S r) _ _

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