English
Base change commutes with binary products: if f and g admit a base change along S, then the base-changed product map f.prodMap g is again a base-change.
Русский
Изменение базы коммутирует с бинарными произведениями: если отображения f и g допускают изменение базы относительно S, то полученное отображение f.prodMap g также является изменением базы.
LaTeX
$$$IsBaseChange\\; S\\; (f.\\mathrm{prodMap}\\; g)$$$
Lean4
/-- Base change commutes with binary products. -/
theorem prodMap {M N M' N' : Type*} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [AddCommMonoid M']
[AddCommMonoid N'] [Module R M'] [Module R N'] [Module S M'] [Module S N'] [IsScalarTower R S M']
[IsScalarTower R S N'] (f : M →ₗ[R] M') (g : N →ₗ[R] N') (hf : IsBaseChange S f) (hg : IsBaseChange S g) :
IsBaseChange S (f.prodMap g) :=
by
apply of_equiv (TensorProduct.prodRight R _ S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv)
intro p
simp [equiv_tmul]
