English
A lemma about tmul and mk' giving a relation in the tensor product with localization.
Русский
Лемма о tmul и mk' задаёт соотношение в тензорном произведении локализации.
LaTeX
$$IsLocalization.tmul_mk'_note$$
Lean4
theorem tmul_mk' (M : Submonoid R) [IsLocalization M A] (s : S) (x : R) (y : M) :
s ⊗ₜ IsLocalization.mk' A x y =
IsLocalization.mk' (S ⊗[R] A) (algebraMap R S x * s)
⟨algebraMap R S y.1, Algebra.mem_algebraMapSubmonoid_of_mem _⟩ :=
by
rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_apply, Algebra.algebraMap_self, RingHomCompTriple.comp_apply,
tmul_one_eq_one_tmul, tmul_mul_tmul, mul_one, mul_comm, IsLocalization.mk'_spec', algebraMap_apply,
Algebra.algebraMap_self, RingHom.id_apply, ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
