instCompatibleSMulRat — Mathlib

English

If A and B satisfy the CompatibleSMul assumptions, then the lid construction yields a canonical isomorphism A ⊗_R B ≃_S A.

Русский

Если A и B удовлетворяют условиям совместимой SMul, то конструкция lid даёт каноническое изоморфизм A ⊗_R B ≃_S A.

LaTeX

$$$\\mathrm{lidOfCompatibleSMul}\\; R\\; S\\; A : S \\otimes_R A \\cong_S A$$$

Lean4

instance {R M N : Type*} [CommSemiring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module ℚ M]
    [Module ℚ N] : CompatibleSMul R ℚ M N where
  smul_tmul q m
    n :=
    by
    suffices q.den • ((q • m) ⊗ₜ[R] n) = q.den • (m ⊗ₜ[R] (q • n)) from
      smul_right_injective (M ⊗[R] N) (c := q.den) q.den_nz <| by norm_cast
    rw [smul_tmul', ← tmul_smul, ← smul_assoc, ← smul_assoc, nsmul_eq_mul, Rat.den_mul_eq_num]
    norm_cast
    rw [smul_tmul]

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