isLocalization_iff_isPushout — Mathlib

English

If A is a localization of R, the tensoring of an A-module with A over R is naturally equivalent to the identity; the module Lid construction yields an isomorphism A ⊗_R M ≃_A M.

Русский

Если A — локализация от R, тензорное произведение модуля над R с A эквивалентно идентичности: A ⊗_R M ≃_A M.

LaTeX

$$$A\otimes_R M \cong_A M$$$

Lean4

theorem isLocalization_iff_isPushout : IsLocalization (Algebra.algebraMapSubmonoid T S) B ↔ IsPushout R T A B :=
  by
  rw [Algebra.IsPushout.comm, Algebra.isPushout_iff, ← isLocalizedModule_iff_isLocalization]
  rw [← isLocalizedModule_iff_isBaseChange (S := S)]

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