moduleLid — Mathlib

English

If A is a localization of R, tensoring two A-algebras over A is the same as tensoring them over R; i.e., B ⊗_A C ≃_A B ⊗_R C.

Русский

Если A — локализация от R, тензорное произведение двух A-алгебр над A эквивалентно произведению над R; B ⊗_A C ≃_A B ⊗_R C.

LaTeX

$$$B \otimes_A C \cong_A B \otimes_R C$$$

Lean4

/-- If `A` is a localization of `R`, tensoring an `A`-module with `A` over `R` does nothing. -/
noncomputable def moduleLid : A ⊗[R] M₁ ≃ₗ[A] M₁ :=
  have := tensorProduct_compatibleSMul S A A M₁
  (equivOfCompatibleSMul R A A M₁).symm ≪≫ₗ TensorProduct.lid _ _

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