English
For a base-change φ: S →ₐ[R] S' and a polynomial law f: M →ₚₗ[R] N, the base-change of f commutes with φ in the sense that applying φ before or after the rTensor yields the same result.
Русский
Для базового перехода φ: S →ₐ[R] S' и полиномального закона f: M →ₚₗ[R] N, переход по основанию commuting с φ: применение φ до или после rTensor даёт одинаковый результат.
LaTeX
$$$\forall f, S, S', φ:\; (φ^{\mathrm{rTensor}})(f_S(x)) = f_{S'}((φ^{\mathrm{rTensor}})(x))$ for all $x \in S \otimes_R M$.$$
Lean4
@[local simp]
theorem isCompat_apply' {R : Type u} [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M] {N : Type*}
[AddCommMonoid N] [Module R N] {f : M →ₚₗ[R] N} {S : Type u} [CommSemiring S] [Algebra R S] {S' : Type u}
[CommSemiring S'] [Algebra R S'] (φ : S →ₐ[R] S') (x : S ⊗[R] M) :
(φ.toLinearMap.rTensor N) ((f.toFun' S) x) = (f.toFun' S') (φ.toLinearMap.rTensor M x) := by
simpa only using congr_fun (f.isCompat' φ) x
