lidOfCompatibleSMul — Mathlib

English

Under broader compatibility assumptions, there is an isomorphism between A ⊗_S B and A ⊗_R B compatible with both SMul directions.

Русский

При более широких предпосылках совместимости существует изоморфизм между A ⊗_S B и A ⊗_R B, совместимый с обеими направлениями SMul.

LaTeX

$$$\\mathrm{equivOfCompatibleSMul}\\;[R]\\;[S]\\;A\\;B : A \\otimes_S B \\cong A \\otimes_R B$$$

Lean4

/-- If the R- and S- action on S and A satisfy `CompatibleSMul` both ways,
then `S ⊗[R] A` is canonically isomorphic to `A`. -/
def lidOfCompatibleSMul : S ⊗[R] A ≃ₐ[S] A :=
  (equivOfCompatibleSMul R S S A).symm.trans (TensorProduct.lid _ _)

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